Compositional verification of smart contracts through communication abstraction

DOI10.1007/978-3-030-88806-0_21zbMath1497.68321arXiv2107.08583OpenAlexW3206384689MaRDI QIDQ2145351

Richard Trefler, Maria Christakis, Arie Gurfinkel, Scott Wesley, Valentin Wüstholz, Jorge A. Navas

Publication date: 17 June 2022

Full work available at URL: https://arxiv.org/abs/2107.08583

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Uses Software

• SeaHorn
• Manticore
• solc-verify
• VerX

Cites Work

• Unnamed Item
• Unnamed Item
• An axiomatic proof technique for parallel programs
• Parameterized compositional model checking
• Towards Efficient Parameterized Synthesis
• All for the Price of Few
• Reasoning about systems with many processes
• Model Checking Software
• On Reasoning About Rings
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Compositional verification of smart contracts through communication abstraction