FunFrog

FunFrog is a bounded model checker of C using interpolation-based function summaries. FunFrog uses Craig interpolation to extract function summaries and reuses them in subsequent verification runs as a means of over-approximation of the precise functions' behavior.

To deal with spurious errors, which are possible due to the over-approximation, FunFrog employs a counter-example guided refinement strategy to identify too coarse summaries responsible for the error trace and replaces those with precise behavior representation in the next iteration.

FunFrog is implemented in the CProver framework (www.cprover.org). For satisfiability checks as well as for interpolant generation, FunFrog uses PeRIPLO. 

 

Published papers:

  1. Interpolation-based Function Summaries in Bounded Model Checking, Sery, O.; Fedyukovich, G.; Sharygina, N. , Haifa Verification Conference (HVC), Haifa, Israel, Springer (2011)
  2. FunFrog: Bounded Model Checking with Interpolation-based Function Summarization, Fedyukovich, G.; Sery, O.; Sharygina, N. , 10th International Symposium on Automated Technology for Verification and Analysis (ATVA), Thiruvananthapuram, India (2012)
  3. Towards completeness in Bounded Model Checking through Automatic Recursion Depth Detection, Fedyukovich, G.; Sharygina, N. , Brazilian Symposium on Formal Methods (SBMF), Maceio, Brazil (2014)
  4. Symbolic Detection of Assertion Dependencies for Bounded Model Checking, Fedyukovich, G., A. D'Iddio Callia, Hyvärinen A., and Sharygina N. , 18th International Conference on Fundamental Approaches to Software Engineering (FASE), London, UK (2015)