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.
- Interpolation-based Function Summaries in Bounded Model Checking, , Haifa Verification Conference (HVC), Haifa, Israel, Springer (2011)
- FunFrog: Bounded Model Checking with Interpolation-based Function Summarization, , 10th International Symposium on Automated Technology for Verification and Analysis (ATVA), Thiruvananthapuram, India (2012)
- Towards completeness in Bounded Model Checking through Automatic Recursion Depth Detection, , Brazilian Symposium on Formal Methods (SBMF), Maceio, Brazil (2014)
- Symbolic Detection of Assertion Dependencies for Bounded Model Checking, , 18th International Conference on Fundamental Approaches to Software Engineering (FASE), London, UK (2015)