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

Hardware verification algorithms were previously modified to suit software verification and implemented in CPAchecker. These algorithms iteratively compute interpolants to overapproximate reachable state space and eventually converge to invariant. They use interpolation in a so-called forward fashion to overapproximate reachable states from initial states. Dual Approximated Reachability algorithm also uses interpolants to overapproximate states that can reach assertion-violating states. It combines information from both forward and backward interpolation sequences to converge faster. In the talk, we briefly explain the main idea of the algorithm, show practical obstacles in the CPAchecker implementation that we overcame and present the final results of the algorithm’s performance.

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