FunFrog: Bounded Model Checking with Interpolation-based Function Summarization

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F12%3A10124356" target="_blank" >RIV/00216208:11320/12:10124356 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-642-33386-6_17" target="_blank" >http://dx.doi.org/10.1007/978-3-642-33386-6_17</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-33386-6_17" target="_blank" >10.1007/978-3-642-33386-6_17</a>

Jazyk výsledku

angličtina

Název v původním jazyce

FunFrog: Bounded Model Checking with Interpolation-based Function Summarization

Popis výsledku v původním jazyce

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. Experimentalevaluation demonstrates competitiveness of FunFrog with respect to state-of-the-art software model checkers.

Název v anglickém jazyce

FunFrog: Bounded Model Checking with Interpolation-based Function Summarization

Popis výsledku anglicky

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. Experimentalevaluation demonstrates competitiveness of FunFrog with respect to state-of-the-art software model checkers.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2012

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Lecture Notes in Computer Science

ISSN

0302-9743

e-ISSN

—

Svazek periodika

2012

Číslo periodika v rámci svazku

7561

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

5

Strana od-do

203-207

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—