Henrik Wachowitz from LMU will give a talk in the elite program’s special lecture series. The title of the talk is “Usability and Infrastructure: Challenges in Software Verification” and it will take place in room 1055N at 4PM on 28th November 2024.

Abstract

In this talk, I explore the field of automatic software verification and address a central question: why hasn’t formal verification gained wider adoption? My research emphasizes usability, seeking to make software verification more intuitive and accessible for developers.

I will introduce FM-Weck, a tool designed to streamline the exploration and integration of community tools by leveraging terminology familiar to software verification researchers. Additionally, I will present the CoVeriTeam GUI, a no-code framework that empowers users to build cooperative verification workflows effortlessly.

As part of the infrastructure challenges, I will present CPA-Daemon, a framework that makes the software verifier CPAchecker accessible via gRPC. This framework enables stateful verification, opening new possibilities for distributed and persistent analysis.

Finally, I will illustrate these themes through two key use cases: large-scale distributed software verification and the international Software Verification Competition (SV-COMP). These examples highlight the ongoing challenges and opportunities in advancing both the usability and infrastructure of software verification tools.

Biography

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