Am 16.01.2025 hält Marian Lingsch-Rosenfeld von der LMU ab 16:00 Uhr einen Gastvortrag in der Ringvorlesung des Elitestudiengangs Software Engineering. Der Vortrag findet in Raum 1055N statt und hat den Titel "Software Verification Witnesses". Zum Vortrag sind alle herzlich eingeladen.

Abstract:

Ensuring that software meets desired quality standards is a crucial aspect of the development process. A wide variety of approaches and tools exist for this purpose, with four important paradigms: Testing, Automatic Verification, Deductive Verification, and Interactive Theorem Provers. Each paradigm has unique strengths and limitations with notable tools including, but not limited to, AFL++ for Testing, Dafny and Frama-C for Deductive Verification, CPAchecker and UAutomizer for Automatic Verification, and KIV and Coq for Interactive Theorem Proving, between many others. Different tools differ not only in their underlying formalisms, which influence how they present proofs or counterexamples, but also in their preferred methods of interacting with users.

In this talk I will present an idea which has emerged in the last decade to aid in tool interoperability and user interaction: Software Verification Witnesses. Witnesses are a machine-readable data format that allows tools to encode information about their verification process as invariants for correctness arguments or paths through a program leading to an error.

Marian Lingsch-Rosenfeld ist Absolvent des Elitestudiengangs und forscht bei Prof. Beyer an der LMU.