2 papers
cs.PL2021
Rich Specifications for Ethereum Smart Contract Verification
Christian Bräm, Marco Eilers, Peter Müller +2
Smart contracts are programs that execute inside blockchains such as Ethereum to manipulate digital assets. Since bugs in smart contracts may lead to substantial financial losses,…
cs.LO2020
Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
Christoph Sprenger, Tobias Klenze, Marco Eilers +4
Lighthouse projects such as CompCert, seL4, IronFleet, and DeepSpec have demonstrated that full verification of entire systems is feasible by establishing a refinement relation bet…