@conference { Ondrej Sery; Gri,
	title = {Incremental Upgrade Checking by Means of Interpolation-based Function Summaries},
	booktitle = {Twelfth International Conference on Formal Methods in Computer-Aided Design (FMCAD)},
	year = {2012},
	note = {To appear at the conference. The pdf-version is not final.},
	address = {Cambridge, UK},
	author = {Sery, O. and Grigory Fedyukovich and Natasha Sharygina}
}
@conference {148,
	title = {Interpolation-based Function Summaries in Bounded Model Checking},
	booktitle = {Haifa Verification Conference (HVC)},
	year = {2011},
	publisher = {Springer},
	organization = {Springer},
	address = {Haifa, Israel},
	abstract = {<p style="text-align: justify;"><span >During model checking of software against various specifications,\&nbsp;it is often the case that the same parts of the program have to be modeled/verified multiple times.\&nbsp;To reduce the overall verification effort, this paper proposes a new technique that extracts function summaries after the initial successful verification run,\&nbsp;and then uses them for more efficient subsequent analysis of the other specifications.\&nbsp;Function summaries are computed as over-approximations using Craig interpolation, a mechanism which is well-known to preserve the most relevant information,\&nbsp;and thus tend to be a good substitute for the functions that were examined in the previous verification runs.\&nbsp;In our summarization-based verification approach, the spurious behaviors introduced as a side effect of the over-approximation,\&nbsp;are ruled out automatically by means of the counter-example guided refinement of the function summaries.\&nbsp;We implemented interpolation-based summarization in our FunFrog tool, and compared it with several state-of-the-art software model checking tools.\&nbsp;Our experiments demonstrate the feasibility of the new technique and confirm its advantages on the large programs.</span></p>
},
	author = {Sery, O. and Grigory Fedyukovich and Natasha Sharygina}
}
