HiFrog is a bounded Model Checker for C programming language which is based on  SMT solver OpenSMT2.  HiFrog exploits the CProver framework and inherits some of its options.

 The system currently supports verication based on the quantier-free theories of linear real arithmetics (QF_LRA) and uninterpreted functions (QF_UF), in addition to propositional logic (QF_BOOL).

HiFrog as interpolating incremental C verifier offers support for the following features:

  • Various interpolants for QF_BOOL, QF-LRA, QF-UF
  • Injecting summaries ( User-Provided Summaries)
  • Automatic recursion unwinding
  • Assertion optimization
  • Tuning the Strength of Summaries
  • Tuning the Size of Summaries
  • Counterexamples