FunFrog: Bounded Model Checking with Interpolation-based Function Summarization
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
FunFrog: Bounded Model Checking with Interpolation-based Function Summarization
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2012
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Lecture Notes in Computer Science
ISSN
0302-9743
e-ISSN
—
Volume of the periodical
2012
Issue of the periodical within the volume
7561
Country of publishing house
DE - GERMANY
Number of pages
5
Pages from-to
203-207
UT code for WoS article
—
EID of the result in the Scopus database
—