State space reduction strategies for model checking concurrent C programs - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Access content directly
Conference Papers Year : 2015

State space reduction strategies for model checking concurrent C programs

Abstract

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.
Fichier principal
Vignette du fichier
MLBHB-vecos15.pdf (524.57 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

cea-01844041 , version 1 (18-01-2019)

Identifiers

  • HAL Id : cea-01844041 , version 1

Cite

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⟩
69 View
99 Download

Share

Gmail Facebook Twitter LinkedIn More