State space reduction strategies for model checking concurrent C programs

Conference of 9th Workshop on Verification and Evaluation of Computer and Communication Systems, VECoS 2015 ; Conference Date: 10 September 2015 Through 11 September 2015; Conference Code:115655International audienceModel checking is an effective technique for uncovering subtle errors in concurrent systems. Unfortunately, the state space explosion is the main bottleneck in model checking tools. Here we propose a state space reduction technique for model checking concurrent programs written in C. The reduction technique consists in an analysis phase, which defines an approximate agglomeration predicate. This latter states whether a statement can be agglomerated or not. We implement this predicate using a syntactic analysis, as well as a semantic analysis based on abstract interpretation. We show the usefulness of using agglomeration technique to reduce the state space, as well as to generate an abstract TLA+ specification from a C program