HiFrog

HiFrog is a bounded model checker for the C programming language whose functionality is interleaved with SMT reasoning for various computational tasks. In particular, it uses SMT solving and various SMT interpolating procedures for verification and program abstraction.

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 quantifier-free theories of four encoding precisions through SMT:

  • Equality with Uninterpreted Functions (EUF),
  • Linear Real Arithmetic (LRA),
  • Linear Real Arithmetic (LIA),
  • Propositional Logic (PROP).

For satisfiability checks as well as for interpolant generation HiFrog uses SMT solver OpenSMT2. For pre-processing and symbolic encoding of C, HiFog uses the CProver framework and inherits some of its options. 

HiFrog is implemented in C++ and the current implementation lives at the branch 'hifrog'  of the repository https://github.com/usi-verification-and-security/upprover

 

Publications:

  1. HiFrog: SMT-based Function Summarization for Software Verification L. Alt, S. Asadi, H. Chockler, K. Even, G. Fedyukovich , A. Hyvarinen, and N. Sharygina, TACAS 2017. link, pdf, demo, supplemental material
  2. Theory Refinement for Program Verification A. Hyvarinen, S. Asadi, K. Even-Mendoza, G. Fedyukovich, and N. Sharygina, SAT 2017. pdf, supplemental material 
  3. Duality-based interpolation for quantifier-free equalities and uninterpreted functions L. Alt, A. Hyvarinen, S. Asadi, and N. Sharygina , FMCAD 2017. pdf 
  4. Function Summarization Modulo Theories S. Asadi, M. Blicha, A. Hyvarinen, G. Fedyukovich, K. Even, N. Sharygina, and H. Chockler, LPAR 2018. pdf, supplemental material
  5. Lattice-Based Refinement in Bounded Model Checking K. Even-Mendoza, , S. Asadi, A. Hyvarinen,  H. Chockler, and N. Sharygina, VSTTE 2018. pdf
  6. Lattice-based SMT for Program Verification K Even-Mendoza, A. Hyvärinen, H. Chockler, N. Sharygina, Memocode 2019. pdf