|Title||HiFrog: SMT-based Function Summarization for Software Verification|
|Publication Type||Conference Paper|
|Year of Publication||2017|
|Authors||Alt, Leonardo, Asadi Sepideh, Chockler Hana, Even Mendoza Karine, Fedyukovich Grigory, Hyvärinen Antti E. J., and Sharygina Natasha|
|Conference Name||23rd 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.