Model Checker Execution Reports
Rodrigo Casta\~no, Victor Braberman, Diego Garbervetsky, Sebastian, Uchitel

TL;DR
This paper introduces execution reports for software model checkers, providing insights into incomplete checks by formalizing and implementing a method to analyze analyzed traces and safe cones, enhancing understanding of model checking processes.
Contribution
It formalizes execution reports for model checkers, enabling access to information on incomplete checks, and demonstrates this approach with CPAchecker.
Findings
Execution reports reveal detailed information about analyzed traces.
The approach improves understanding of incomplete verification results.
Empirical evaluation shows practical utility of execution reports.
Abstract
Software model checking constitutes an undecidable problem and, as such, even an ideal tool will in some cases fail to give a conclusive answer. In practice, software model checkers fail often and usually do not provide any information on what was effectively checked. The purpose of this work is to provide a conceptual framing to extend software model checkers in a way that allows users to access information about incomplete checks. We characterize the information that model checkers themselves can provide, in terms of analyzed traces, i.e. sequences of statements, and safe cones, and present the notion of execution reports, which we also formalize. We instantiate these concepts for a family of techniques based on Abstract Reachability Trees and implement the approach using the software model checker CPAchecker. We evaluate our approach empirically and provide examples to illustrate the…
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.
