Conditional Model Checking
Dirk Beyer, Thomas A. Henzinger, M. Erkan Keremoglu, Philipp, Wendler

TL;DR
This paper introduces a reformulation of software model checking as a conditional process that reports partial verification results, enabling iterative refinement and improved coverage even when full verification fails.
Contribution
It proposes a novel conditional model checking approach that summarizes verification work and guides iterative checking to enhance coverage and efficiency.
Findings
Conditional model checkers can report useful partial results.
Repeated application improves verification coverage.
Performance and state-space coverage are significantly enhanced.
Abstract
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 P ---usually a state predicate--- such that the program satisfies the specification under the condition P ---that is, as long as the program does not leave states in which P is…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
