FunFrog: Bounded Model Checking with Interpolation-based Function Summarization

Abstract:

This paper presents FunFrog, a tool that implements a function summarization approach for software bounded model checking. It uses interpolation-based function summaries as over-approximation of function calls. In every successful verification run, FunFrog generates function summaries of the analyzed program functions and reuses them to reduce the complexity of the successive verification. Experimental evaluation demonstrates competitiveness of FunFrog with respect to state-of-the-art software model checkers.

Notes:

• BibTex

@inproceedings { Ondrej Sery; Gri,
	title = {FunFrog: Bounded Model Checking with Interpolation-based Function Summarization},
	booktitle = {Tenth International Symposium on Automated Technology for Verification and Analysis (ATVA)},
	year = {2012},
	note = {To appear at the conference. The pdf-version is not final.},
	address = {Thiruvananthapuram, India},
	URL = {publications/ondrej-sery-grigory-fedyukovich-natasha-sharygina-2012-funfrog-bounded-model-checking-with-interpolation-based-function-summarization},
	author = {Ondrej Sery and  Grigory Fedyukovich and  Natasha Sharygina}
}