Termite

Termite is a tool to check termination of programs in the LLVM IR. It uses pagai as invariant generator and Z3 as SMT-solver.

Install and dependencies

With opam

Using opam, you can install (most of) the dependencies easily. See the install instructions here.

Dependencies

External dependencies:

• Z3
• Pagai

Ocaml dependencies:

• batteries-included
• Zarith
• ocamlgraph
• llvmgraph
• z3overlay
• llvm2smt