Back to overview

HiFrog: SMT-based Function Summarization for Software Verification

Type of publication Peer-reviewed
Publikationsform Proceedings (peer-reviewed)
Author Leonardo Alt Sepideh Asadi Hana Chockler Karine Even-Mendoza Grigory Fedyukovich Antti E. J. Hy,
Project Guiding SMT-Based Interpolation for Program Verification
Show all

Proceedings (peer-reviewed)

Title of proceedings Tools and Algorithms for the Construction and Analysis of Systems
DOI 10.1007/978-3-662-54580-5_12

Open Access

Type of Open Access Website


Function summarization can be used as a means of incremental verification 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.