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

doi:10.1007/978-3-662-54580-5_12

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 proceeding › Conference paper › peer-review

14 Citations (Scopus)

708 Downloads (Pure)

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 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 language	English
Title of host publication	Tools 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
Publisher	Springer
Pages	207-213
Number of pages	7
Volume	10206
ISBN (Electronic)	978-3-662-54580-5
DOIs	https://doi.org/10.1007/978-3-662-54580-5_12
Publication status	Published - 24 Apr 2017

Access to Document

10.1007/978-3-662-54580-5_12

mainLicence: Unspecified

Cite this

Alt, L., Asadi, S., Chockler, H., Even-Mendoza, K., Fedyukovich, G., Hyvärinen, A. E. J., & Sharygina, N. (2017). HiFrog: SMT-based Function Summarization for Software Verification. In Tools 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 (Vol. 10206, pp. 207-213). Springer. https://doi.org/10.1007/978-3-662-54580-5_12

Alt, Leonardo ; Asadi, Sepideh ; Chockler, Hana et al. / HiFrog: SMT-based Function Summarization for Software Verification. Tools 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. Vol. 10206 Springer, 2017. pp. 207-213

@inbook{aa6a1be1e6e64649b43a42618d9f45c5,

title = "HiFrog: SMT-based Function Summarization for Software Verification",

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 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.",

author = "Leonardo Alt and Sepideh Asadi and Hana Chockler and Karine Even-Mendoza and Grigory Fedyukovich and Hyv{\"a}rinen, {Antti E. J.} and Natasha Sharygina",

year = "2017",

month = apr,

day = "24",

doi = "10.1007/978-3-662-54580-5_12",

language = "English",

volume = "10206",

pages = "207--213",

booktitle = "Tools 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",

publisher = "Springer",

}

Alt, L, Asadi, S, Chockler, H , Even-Mendoza, K, Fedyukovich, G, Hyvärinen, AEJ & Sharygina, N 2017, HiFrog: SMT-based Function Summarization for Software Verification. in Tools 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. vol. 10206, Springer, pp. 207-213. https://doi.org/10.1007/978-3-662-54580-5_12

HiFrog: SMT-based Function Summarization for Software Verification. / Alt, Leonardo; Asadi, Sepideh; Chockler, Hana et al.
Tools 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. Vol. 10206 Springer, 2017. p. 207-213.

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

TY - CHAP

T1 - HiFrog: SMT-based Function Summarization for Software Verification

AU - Alt, Leonardo

AU - Asadi, Sepideh

AU - Chockler, Hana

AU - Even-Mendoza, Karine

AU - Fedyukovich, Grigory

AU - Hyvärinen, Antti E. J.

AU - Sharygina, Natasha

PY - 2017/4/24

Y1 - 2017/4/24

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-662-54580-5_12

DO - 10.1007/978-3-662-54580-5_12

M3 - Conference paper

VL - 10206

SP - 207

EP - 213

BT - Tools 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

PB - Springer

ER -

Alt L, Asadi S, Chockler H , Even-Mendoza K, Fedyukovich G, Hyvärinen AEJ et al. HiFrog: SMT-based Function Summarization for Software Verification. In Tools 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. Vol. 10206. Springer. 2017. p. 207-213 doi: 10.1007/978-3-662-54580-5_12

HiFrog: SMT-based Function Summarization for Software Verification

Abstract

Access to Document

Fingerprint

Cite this