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.

Sections:
Architecture
Tutorial
Download 

[1][2]

References

  1. Interpolation-based Function Summaries in Bounded Model Checking, Sery, O.; Fedyukovich, G.; Sharygina, N. , Haifa Verification Conference (HVC), Haifa, Israel, Springer (2011)
  2. Function Summaries in Software Upgrade Checking, Fedyukovich, G.; Sery, O.; Sharygina, N. , Haifa Verification Conference (HVC), Volume 7261, Haifa, Israel, Springer (2011)