University of Illinois Urbana-Champaign

Academic Unit
Collection
Author(s)
Keyword(s)
Type of Resource
Showing 1–30 of 56 items
Thumbnail for A general approach to define binders using matching logic
A general approach to define binders using matching logic
Chen, Xiaohong; Roşu, Grigore

Thumbnail for Matching μ-Logic
Matching μ-Logic
Chen, Xiaohong; Roşu, Grigore

Thumbnail for Verification of Casper in the Coq Proof Assistant
Verification of Casper in the Coq Proof Assistant
Palmskog, Karl; Gligoric, Milos; Pena, Lucas; Moore, Brandon; Roşu, Grigore

Thumbnail for Statistical Model Checking of RANDAO’s Resilience Against Pre-computed Reveal Strategies
Statistical Model Checking of RANDAO’s Resilience Against Pre-computed Reveal Strategies
Alturki, Musab A.; Roşu, Grigore

Thumbnail for End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
Park, Daejun; Zhang, Yi; Roşu, Grigore

Thumbnail for Open Problems and Challenges 2017
Open Problems and Challenges 2017
Roşu, Grigore

Thumbnail for IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics
IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics
Kasampalis, Theodoros; Guth, Dwight; Moore, Brandon; Serbanuta, Traian; Serbanuta, Virgil; Filaretti, Daniele; Roşu, Grigore; Johnson, Ralph

Thumbnail for IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics
IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics
Kasampalis, Theodoros; Guth, Dwight; Moore, Brandon; Serbanuta, Traian; Serbanuta, Virgil; Filaretti, Daniele; Roşu, Grigore; Johnson, Ralph

Thumbnail for Applicative matching logic
Applicative matching logic
Chen, Xiaohong; Roşu, Grigore

Thumbnail for Initial Algebra Semantics in Matching Logic
Initial Algebra Semantics in Matching Logic
Chen, Xiaohong; Lucanu, Dorel; Roşu, Grigore

Thumbnail for Evolution-aware runtime verification
Evolution-aware runtime verification
Legunsen, Owolabi

Thumbnail for A formal semantics of P4 and applications
A formal semantics of P4 and applications
Kheradmand, Ali

Thumbnail for Toward automatic programming
Toward automatic programming
Radoi, Cosmin A

Thumbnail for Learning based programming
Learning based programming
Rizzolo, Nicholas

Thumbnail for Rewriting-based model checking methods
Rewriting-based model checking methods
Bae, Kyungmin

Thumbnail for KEVM: A Complete Semantics of the Ethereum Virtual Machine
KEVM: A Complete Semantics of the Ethereum Virtual Machine
Everett Hildenbrandt; Saxena, Manasvi; Xiaoran Zhu; Rodrigues, Nishant; Philip Daian; Guth, Dwight; Roşu, Grigore

Thumbnail for IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
Kasampalis, Theodoros; Guth, Dwight; Moore, Brandon; Serbanuta, Traian Florin; Zhang, Yi; Filaretti, Daniele; Serbanuta, Virgil; Johnson, Ralph; Roşu, Grigore

Thumbnail for IsaK: A Complete Semantics of K
IsaK: A Complete Semantics of K
Li, Liyi; Gunter, Elsa L.

Thumbnail for Trustworthy Program Verification via Proof Generation
Trustworthy Program Verification via Proof Generation
Lin, Zhengyao; Chen, Xiaohong; Trinh, Minh-Thai; Wang, John; Rosu, Grigore

Thumbnail for Making Formal Verification Trustworthy via Proof Generation
Making Formal Verification Trustworthy via Proof Generation
Lin, Zhengyao; Chen, Xiaohong; Trinh, Minh-Thai; Wang, John; Rosu, Grigore

Thumbnail for An Interactive Theorem Prover for Matching Logic with Proof Object Generation
An Interactive Theorem Prover for Matching Logic with Proof Object Generation
Lin, Zhengyao; Chen, Xiaohong; Rosu, Grigore

Thumbnail for Guarded Matching Logic is Decidable
Guarded Matching Logic is Decidable
Rodrigues, Nishant; Chen, Xiaohong; Rosu, Grigore

Thumbnail for Towards A Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic
Towards A Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic
Xiaohong Chen; Minh-Thai Trinh; Nishant Rodrigues; Lucas Pena; Grigore Rosu

Thumbnail for Foundations for practical network verification
Foundations for practical network verification
Kheradmand, Ali

Thumbnail for Semantics-based program verification
Semantics-based program verification
Park, Daejun

Thumbnail for Preparation-free and comprehensive runtime verification tool for testing Java programs
Preparation-free and comprehensive runtime verification tool for testing Java programs
Lee, Choonghwan

Thumbnail for Matching Logic Proofs Meet Succinct Cryptographic Proofs
Matching Logic Proofs Meet Succinct Cryptographic Proofs
Bailey, Bolton; Chen, Xiaohong; Fiedler, Adam; Malvai, Harjasleen; Miller, Andrew; Mishra, Pratyush; Rodrigues, Nishant; Rosu, Grigore • 2024

Thumbnail for Coinductive program verification
Coinductive program verification
Moore, Brandon Michael

Thumbnail for Translation validation for compilation verification
Translation validation for compilation verification
Kasampalis, Theodoros

Thumbnail for Nelson Oppen combination as a rewrite theory
Nelson Oppen combination as a rewrite theory
Rodrigues, Nishant