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.

Matthias Kettl

LMU Munich