HiFrog is a bounded Model Checker for C programming language which is based on SMT solver OpenSMT2.
HiFrog is a fully featured function-summarization-based model checker that uses SMT as the modeling and summarization language for verifying a set of user-defined assertions in a single program.
The tool supports quantier-free theories of three encoding precisions through SMT:
- Equality with Uninterpreted Functions (EUF),
- Linear Real Arithmetic (LRA),
- Linear Real Arithmetic (LIA),
- Propositional Logic(PROP).
HiFrog exploits the CProver framework and inherits some of its options.
