@conference {269, title = {HiFrog: SMT-based Function Summarization for Software Verification}, booktitle = {23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, year = {2017}, publisher = {Springer}, organization = {Springer}, address = {Uppsala}, abstract = {

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.

}, url = {https://link.springer.com/chapter/10.1007/978-3-662-54580-5_12 }, author = {Leonardo Alt and Sepideh Asadi and Hana Chockler and Karine Even Mendoza and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} }