3 papers
cs.PL2026
Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)
Hongyi Ling, Thibault Dardinier, Ellen Arlt +1
Automated program verifiers are often organized into a front-end, which encodes an input program into an intermediate verification language (IVL), and a back-end, which proves that…
cs.SE2025
Toward Practical Deductive Verification: Insights from a Qualitative Survey in Industry and Academia
Lea Salome Brugger, Xavier Denis, Peter Müller
Deductive verification is an effective method to ensure that a given system exposes the intended behavior. In spite of its proven usefulness and feasibility in selected projects, d…
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,…