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.

Daniel Baier

Ludwig Maximilian University of Munich

Germany

PhD-student of Prof. Dr. Dirk Beyer, at the SoSy-Lab, LMU Munich.