A game semantics framework delivers the first sound and complete open-world assertion checking for Ethereum smart contracts, implemented as YulTracer which achieves perfect recall and precision on reentrancy benchmarks and real-world exploits.
hub
A Tool for Checking ANSI-C Pro- grams
5 Pith papers cite this work, alongside 1,389 external citations. Polarity classification is still indexing.
5
Pith papers citing it
1,389
external citations · OpenAlex
hub tools
representative citing papers
HDL defines dynamic theories with lifting and combination operations, proves soundness and relative completeness in Isabelle, and demonstrates the approach on a Java controller steering a differential dynamic logic plant model.
Hardware-faithful verification with a HAL descriptor eliminates all 54 false 16-bit overflow alarms on 123 real IEC 61131-3 programs while preserving robustness proofs.
Kani is a model checker that compiles Rust proof harnesses from MIR to CBMC for bounded verification of safety properties and supports contracts to extend checks to unbounded correctness.
This survey compiles the history, awards, funding, AI integrations, and open challenges of the ESBMC model checker from 2009 to 2026.
citing papers explorer
-
Open-World Assertion Checking for Smart Contracts via Game Semantics
A game semantics framework delivers the first sound and complete open-world assertion checking for Ethereum smart contracts, implemented as YulTracer which achieves perfect recall and precision on reentrancy benchmarks and real-world exploits.
-
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
HDL defines dynamic theories with lifting and combination operations, proves soundness and relative completeness in Isabelle, and demonstrates the approach on a Java controller steering a differential dynamic logic plant model.
-
ESBMC-Arduino: Closing the Deployment Gap for Formal Verification of Open-Hardware PLCs
Hardware-faithful verification with a HAL descriptor eliminates all 54 false 16-bit overflow alarms on 123 real IEC 61131-3 programs while preserving robustness proofs.
-
Kani: A Model Checker for Rust
Kani is a model checker that compiles Rust proof harnesses from MIR to CBMC for bounded verification of safety properties and supports contracts to extend checks to unbounded correctness.
-
ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification
This survey compiles the history, awards, funding, AI integrations, and open challenges of the ESBMC model checker from 2009 to 2026.