ASE 2023
Mon 11 - Fri 15 September 2023 Kirchberg, Luxembourg
Mon 11 Sep 2023 14:30 - 14:35 at Room PT - Lightning Talks

There are many approaches for automated software verification, but they are either imprecise, or they do not scale well to large systems and do not sufficiently leverage parallelization. This leads to large response times, which hinders the integration of software model checking into the development process (continuous integration). We propose a framework for the tool CPAchecker that allows distributing arbitrary CPAs by extending them with only two operators: serialize and deserialize. Serialize takes abstract states and transforms them into messages. Deserialize is the inverse operation and creates abstract states from messages. For successfully deploying a new distributed approach, developers only need to implement a protocol. The talk gives an abstract overview of the framework.

Mon 11 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:30 - 15:00
Lightning Talks[Workshop] CPAchecker at Room PT
14:30
5m
Talk
Enhancing CPAchecker: A Framework for Distributed Analyses
[Workshop] CPAchecker
Matthias Kettl LMU Munich
14:35
5m
Talk
Scaling Formal Verification: Parallel Analysis of Functions
[Workshop] CPAchecker
George Granberry Chalmers University of Technology
14:40
5m
Talk
Dual Approximated Reachability Model Checking in CPAchecker
[Workshop] CPAchecker
Marek Jankola LMU Munich
14:45
5m
Talk
Current State of Memory-Safety Analysis in CPAchecker
[Workshop] CPAchecker
Daniel Baier Ludwig Maximilian University of Munich
14:50
5m
Talk
CPAdaemon: Progress and Demo
[Workshop] CPAchecker
Henrik Wachowitz LMU Munich