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 ( For satisfiability checks as well as for interpolant generation, FunFrog uses PeRIPLO


Published papers:

  1. Interpolation-based Function Summaries in Bounded Model CheckingSery, O.; Fedyukovich, G.; Sharygina, N. , Haifa Verification Conference (HVC), Haifa, Israel, Springer (2011)
  2. FunFrog: Bounded Model Checking with Interpolation-based Function SummarizationFedyukovich, 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 DetectionFedyukovich, G.; Sharygina, N. , Brazilian Symposium on Formal Methods (SBMF), Maceio, Brazil (2014)
  4. Symbolic Detection of Assertion Dependencies for Bounded Model CheckingFedyukovich, G., A. D'Iddio Callia, Hyvärinen A., and Sharygina N. , 18th International Conference on Fundamental Approaches to Software Engineering (FASE), London, UK (2015)