Am 28.11.2024 hält Henrik Wachowitz 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 "Usability and Infrastructure: Challenges in Software Verification". Zum Vortrag sind alle herzlich eingeladen.

 

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.

Henrik Wachowitz ist Absolvent des Elitestudiengangs Software Engineering und promoviert zurzeit bei Prof. Beyer an der LMU.