State space reduction strategies for model checking concurrent C programs - Archive ouverte HAL Access content directly
Conference Papers Year : 2015

State space reduction strategies for model checking concurrent C programs

(1) , (1) , (1) , (2) , (3)
1
2
3

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

Share

Gmail Facebook Twitter LinkedIn More