Overview

 

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 arithmetics (QF_LRA anf QF_LIA) and uninterpreted functions (QF_UF), in addition to propositional logic (QF_BOOL).