Rechercher

[MBL15a] State Space Reduction Strategies for Model Checking Concurrent C Programs

Conférence Internationale avec comité de lecture : 9th Workshop on Verification and Evaluation of Computer and Communication Systems(VECoS'15), September 2015, Vol. 1431, pp.65-76, Series CEUR Workshop Proceedings, Bucharest, Romania,
motcle:
Résumé: 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.

Equipe: systemes surs
Collaboration: CEA-LIST/LASTRE

BibTeX

@inproceedings {
MBL15a,
title="{ State Space Reduction Strategies for Model Checking Concurrent C Programs}",
author=" A. Methni and K. Barkaoui and M. Lemerre and S. Haddad and B. Ben Hedia ",
booktitle="{9th Workshop on Verification and Evaluation of Computer and Communication Systems(VECoS'15)}",
year=2015,
month="September",
series="CEUR Workshop Proceedings",
volume=1431,
pages="65-76",
address="Bucharest, Romania",
}