Announcement: Isabelle/Solidity
Ever wondered how to verify smart contracts written in Solidy? Thanks to our deep embedding of Solidty into Isabelle/HOL, you can now start verifying smart contracts in Isabelle.
Our formalization is available in the Archive of Formal Proofs [1], which can be easily added to Isabelle/HOL. If you want to read a more high-level description of the underlying work, read our conference papers on the topic [3].
References
[1]
D. Marmsoler and A. D. Brucker, “Isabelle/solidity: A deep embedding of solidity in isabelle/HOL,” Archive of Formal Proofs, Jul. 2022,
[2]
D. Marmsoler and A. D. Brucker, “A denotational semantics of Solidity in Isabelle/HOL,” in Software engineering and formal methods (SEFM), R. Calinescu and C. Pasareanu, Eds. Heidelberg: Springer-Verlag, 2021.
[3]
D. Marmsoler and A. D. Brucker, “Conformance testing of formal semantics using grammar-based fuzzing,” in TAP 2022: Tests and proofs, L. Kovacs and K. Meinke, Eds. Heidelberg: Springer-Verlag, 2022.