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.
Mon 11 SepDisplayed 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 |