Model checker execution reports

CASTAÑO RODRIGO; UCHITEL SEBASTIAN; DIEGO GARBERVESTKY; BRABERMAN VICTOR

Conferencia; 32nd IEEE/ACM International Conference on Automated Software Engineerin; 2017

IEEE

Software model checking constitutes an undecidable prob- lem and, as such, even an ideal tool will in some cases fail to give a conclusive answer. In practice, software model check- ers 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 an- alyzed 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 tech- niques 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 execution reports produced and the infor- mation that can be extracted.