 |
Conference papers
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.
Cited literature [28 references]
https://hal-cea.archives-ouvertes.fr/cea-01844041
Contributor : Léna Le Roy <>
Submitted on : Friday, January 18, 2019 - 11:35:24 AM
Last modification on : Thursday, July 2, 2020 - 5:26:02 PM
Contributor : Léna Le Roy <>
Submitted on : Friday, January 18, 2019 - 11:35:24 AM
Last modification on : Thursday, July 2, 2020 - 5:26:02 PM
File
MLBHB-vecos15.pdf
Files produced by the author(s)