HiFrog: SMT-based Function Summarization for Software Verification

Leonardo Alt, Sepideh Asadi, Hana Chockler, Karine Even-Mendoza, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

14 Citations (Scopus)
625 Downloads (Pure)


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 refinement, 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 different SMT precisions have on model-checking.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II
Number of pages7
ISBN (Electronic)978-3-662-54580-5
Publication statusPublished - 24 Apr 2017


Dive into the research topics of 'HiFrog: SMT-based Function Summarization for Software Verification'. Together they form a unique fingerprint.

Cite this