|
 
|
[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:
sys
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", | |
| } | |||
