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, 
  • linear real arithmetics,
  • propositional logic.