Understanding partial verification attempts

RODRIGO CASTAÑO

Buenos Aires

Simposio; 3rd ICSE 2017 PhD and Young Researchers Warm Up Symposium; 2016

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, undecidability is not the only issue.The vast state spaces can lead to exhaustion of resources or impractically long execution times.Unfortunately some instances can take hours of computation only to inform that no counterexample was found. A user facing this situation is confronted with several high-level questions about what the tool actually achieved. Should she retry with a longer time limit? How much longer? Is the verifier making any progress on the instance? Maybe she should try another technique?Previous work has made it possible for tools to generate machine-readable representations of interrupted executions and also to document unsound assumptions made during a verification attempt.Our main hypothesis is that the information gathered during verification can be leveraged by users to make informed decision about future verification and testing efforts.So far we have mostly focused on proposing formally characterized output that responds high-level questions about incomplete verification attempts. For example, we proposed trace-based answers in what we called Execution Reports for the following high-level questions:- Can the incomplete verification attempt provide assurances about concrete executions?- Are there any behaviors that have not yet been examined by the verification tool? Which?We implemented our approach for the family of techniques based on Abstract Reachability Trees.As part of our roadmap, we plan to propose and experiment alternative representations for partial verification results, paying special attention to human-readability and usability.