HiFrog: SMT-based Function Summarization for Software Veri cation

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

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.