Saturation-based incremental LTL model checking with inductive proofs
RiSE will host a talk by András Vörös on May 21, 2015.
|DATE:||Thursday, May 21, 2015|
|VENUE:||Seminar room Zemanek, Favoritenstraße 9-11, 1040 Vienna|
Efficient symbolic and explicit model checking approaches have been developed for the verification of linear time temporal properties. Nowadays, advances resulted in the combination of on-the-fly search with symbolic encoding in a hybrid solution providing many results by now. In this work, we propose a new hybrid approach that leverages the so-called saturation algorithm both as an iteration strategy during the state space generation and in a new incremental fixed-point computation algorithm to compute strongly connected components (SCCs). In addition, our solution works on-the-fly during state space traversal and exploits the decomposition of the model as an abstraction to inductively prove the absence of SCCs with cheap explicit runs on the components. When a proof cannot be shown, the incremental symbolic fixed-point algorithm will find the SCC, if one exists. Evaluation on the models of the Model Checking Contest shows that our approach outperforms similar algorithms for concurrent systems.