FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization

Autor:	Grigory Fedyukovich, Natasha Sharygina, Ondrej Sery
Rok vydání:	2012
Předmět:	Model checking LOOP (programming language) business.industry Computer science Function (mathematics) computer.software_genre Automatic summarization Software Bounded function Data mining business Spurious relationship Algorithm computer Interpolation
Zdroj:	Automated Technology for Verification and Analysis ISBN: 9783642333859 ATVA
DOI:	10.1007/978-3-642-33386-6_17
Popis:	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. To prevent reporting spurious errors , the tool incorporates a counter-example-guided refinement loop. Experimental evaluation demonstrates competitiveness of FunFrog with respect to state-of-the-art software model checkers.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::acee7c1919a4ac6b573246c0ff77f3d9 https://doi.org/10.1007/978-3-642-33386-6_17 Zobrazit plný text záznamu