Lukas Grätz will present his work on a generalisation of the concept of program contracts.
Time and Date: 25 June 2025, 16:00 CEST,
As a follow-up to the March 2024 Lorentz Center workshop on Contract Languages, we will host a series of online presentations and discussions around formal methods with contract languages, aligning with the LTC goal of enabling information exchange between different formal systems.
Dependent Assertion Logic for Modular Software Verification
Abstract. Software is often not designed for formal specification using method contracts (without source refactoring). As solution, we propose dependent assertions, a generalization of method contracts. Our formal- ization uses the propositional dynamic logic PDL but with Dijkstra’s dynamic indices instead of programs inside modal operators. For deduc- tive verification based on a new symbolic execution approach, we outline a sequent calculus to prove basic dependent assertions, including loop invariants. Finally, we can use any (D)PDL solver to prove modular contracts from basic dependencies and other contracts.
If you are interested in joining, drop a mail to Mattias Ulbrich for the link.