HiFrog : SMT-based function summarization for software veri fication

HiFrog is a fully featured function-summarization-based model checker that uses SMT as the modeling and summarization language. 

The tool supports three encoding precisions through SMT:

  • Uninterpreted Functions (QF_UF), 
  • Linear Real Arithmetics (QF_LRA),
  • Propositional Logic.