SMT-based function summarization for software verification


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.