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 Arithmetic (QF_LRA),
- Linear Real Arithmetic (QF_LIA),
- Propositional Logic.
