HiFrog: SMT-based Function Summarization for Software Verification

TitleHiFrog: SMT-based Function Summarization for Software Verification
Publication TypeConference Paper
Year of Publication2017
AuthorsAlt, Leonardo, Asadi Sepideh, Chockler Hana, Even Mendoza Karine, Fedyukovich Grigory, Hyvärinen Antti E. J., and Sharygina Natasha
Conference Name23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Conference LocationUppsala

Abstract. Function summarization can be used as a means of incremental verication based on the structure of the program. HiFrog is a fully featured function-summarization-based model checker that uses SMT as the modeling and summarization language. The tool supports three encoding precisions through SMT: uninterpreted functions, linear real arithmetics, and propositional logic. In addition the tool allows optimized traversal of reachability properties, counter-example-guided summary renement, summary compression, and user-provided summaries. We describe the use of the tool through the description of its architecture and a rich set of features. The description is complemented by an experimental evaluation on the practical impact the dierent SMT precisions have on model-checking.