Enhancing CPAchecker: A Framework for Distributed Analyses
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.
Scaling Formal Verification: Parallel Analysis of Functions
We give an overview of the development of software model checking, a general approach to algorithmic program verification that integrates static analysis, model checking, and deduction. We start with a look backwards and briefly cover some of the important steps in the past decades. The general approach has become a research topic on its own, with a wide range of tools that are based on the approach. Therefore, we discuss the maturity of the research area of software model checking in terms of looking at competitions, at citations, and most importantly, at the tools that were build in this area: we count 76 verification systems for software written in C or Java. We conclude that software model checking has quickly grown to a significant field of research with a high impact on current research directions and tools in software verification. This talk is based on the following joint work with Andreas Podelski: https://doi.org/10.1007/978-3-031-22337-2_27
Dual Approximated Reachability Model Checking in CPAchecker
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.
Current State of Memory-Safety Analysis in CPAchecker
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.
