16:00-17:30

Guest lecture by Marian Lingsch-Rosenfeld from LMU

Marian Lingsch-Rosenfeld from LMU will give a talk in the elite program’s special lecture series. The talk will take place as in room 1055N.

Title

Software Verification Witnesses

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.