Mon 11 Sep 2023 14:45 - 14:50 at Room PT - Lightning Talks
CPAchecker uses a Symbolic Memory Graph (SMG) based analysis to argue about the safety of memory operations. CPAchecker has good results in the MemorySafety category in the SV-COMP23, but no development on the analysis itself has taken place over a long period of time. As a result, the current analysis, based on symbolic execution, is being shifted out and replaced with a new analysis. The new analysis is aimed to be more robust and versatile, as it allows to be run as a explicit-value analysis as well as with symbolic execution and will be extended to be used with CEGAR soon. Preliminary results support this claim.
PhD-student of Prof. Dr. Dirk Beyer, at the SoSy-Lab, LMU Munich.
Mon 11 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 11 Sep
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:30 - 15:00 | |||
14:30 5mTalk | Enhancing CPAchecker: A Framework for Distributed Analyses [Workshop] CPAchecker Matthias Kettl LMU Munich | ||
14:35 5mTalk | Scaling Formal Verification: Parallel Analysis of Functions [Workshop] CPAchecker George Granberry Chalmers University of Technology | ||
14:40 5mTalk | Dual Approximated Reachability Model Checking in CPAchecker [Workshop] CPAchecker Marek Jankola LMU Munich | ||
14:45 5mTalk | Current State of Memory-Safety Analysis in CPAchecker [Workshop] CPAchecker Daniel Baier Ludwig Maximilian University of Munich | ||
14:50 5mTalk | CPAdaemon: Progress and Demo [Workshop] CPAchecker Henrik Wachowitz LMU Munich | ||
