10.1145/2393596.2393664
Beyer, Dirk
Dirk
Beyer
Henzinger, Thomas A
Thomas A
Henzinger0000−0002−2985−7724
Keremoglu, Mehmet
Mehmet
Keremoglu
Wendler, Philipp
Philipp
Wendler
Conditional model checking: A technique to pass information between verifiers
ACM
2012
2018-12-11T11:51:42Z
2020-01-21T13:17:23Z
conference
https://research-explorer.app.ist.ac.at/record/1384
https://research-explorer.app.ist.ac.at/record/1384.json
Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition Ψ - usually a state predicate - such that the program satisfies the specification under the condition Ψ - that is, as long as the program does not leave the states in which Ψ is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before.