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