State space reduction strategies for model checking concurrent C programs

A. Methni (1) , B. Ben Hedia (1) , M. Lemerre (1) , S. Haddad (2) , K. Barkaoui (3)

1 DILS (CEA, LIST) - Département Ingénierie Logiciels et Systèmes
2 LSV - Laboratoire Spécification et Vérification [Cachan]
3 CEDRIC - Centre d'études et de recherche en informatique et communications

Model 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.

Mots clés: Model checking tools; Reduction techniques; State-space explosion; State-space reduction; TLA; Model checking; Concurrent systems; Concurrent program; Abstract interpretations; Syntactics; Semantics; C (programming language); Agglomeration

Domaines: Informatique [cs]

A. Methni, B. Ben Hedia, M. Lemerre, S. Haddad, K. Barkaoui. State space reduction strategies for model checking concurrent C programs. 9th Workshop on Verification and Evaluation of Computer and Communication Systems, VECoS 2015, Sep 2015, Bucharest, Romania. pp.65-75. ⟨cea-01844041⟩