"RIV/00216208:11320/12:10124356" . "Lecture Notes in Computer Science" . "2012" . "Sharygina, Natasha" . "7561" . . . "FunFrog: Bounded Model Checking with Interpolation-based Function Summarization" . "0302-9743" . "FunFrog: Bounded Model Checking with Interpolation-based Function Summarization" . . "5"^^ . "Fedyukovich, Grigory" . . "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."@en . . . . "Function Summarization; Craig Interpolation; Bounded Model Checking"@en . "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." . "10.1007/978-3-642-33386-6_17" . . "11320" . "http://dx.doi.org/10.1007/978-3-642-33386-6_17" . "137405" . . "FunFrog: Bounded Model Checking with Interpolation-based Function Summarization"@en . "RIV/00216208:11320/12:10124356!RIV13-MSM-11320___" . "3"^^ . . "[E93143B5049B]" . "\u0160er\u00FD, Ond\u0159ej" . . . "I" . "1"^^ . . "DE - Spolkov\u00E1 republika N\u011Bmecko" . . "FunFrog: Bounded Model Checking with Interpolation-based Function Summarization"@en . .