Paper Info
Title
Multi-core Model Checking of Large-Scale Reactive Systems Using Different State Representations.
Abstract
Model checking software systems allows to formally verify that their behavior adheres to certain properties. The state explosion problem presents a major obstacle to model checking due to the implied large concrete state spaces. We present an approach to efficient model checking of large-scale reactive systems that aims at a trade-off between the number of verifiable and falsifiable properties and the required analysis time. Our two-phase approach is based on a parallel state space exploration with explicit states for falsifying linear temporal logic (LTL) properties, and an abstract phase reasoning on the entire state space for verifying LTL properties. This two-phase approach enabled us to win the Rigorous Examination of Reactive Systems Challenge (RERS) in 2014 and 2015. We present a detailed evaluation based on 30 different RERS benchmarks regarding both our verification results and the obtainable parallel speedup.
Year
DOI
Venue
2016
10.1007/978-3-319-47166-2_15
Lecture Notes in Computer Science
Field
DocType
Volume
Abstraction model checking,Model checking,Control flow graph,Computer science,Theoretical computer science,Software system,Linear temporal logic,Reactive system,State space,Speedup
Conference
9952
ISSN
Citations 
PageRank 
0302-9743
3
0.40
References 
Authors
16
2
Name
Order
Citations
PageRank
Marc Jasper132.77
Markus Schordan225923.98