Marian Lingsch-Rosenfeld from LMU will give a talk in the elite program’s special lecture series. The title of the talk is “Software Verification Witnesses” and it will take place in room 1055N at 4PM on 21st January 2025.

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.

Biography

Marian Lingsch-Rosenfeld is a graduate of the elite program Software Engineering and does his Ph.D. at LMU’s SoSy-Lab.