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.