Termite - Termination analyser

Research paper

• Termite's algorithm was presented in "Synthesis of ranking functions using extremal counterexamples", PLDI'15
• The author version of the paper is here.
• Bibtex file
• Coming soon : our video presentation for PLDI.

Source code/ Experimental results

• The invariant generator we use is Pagai
• Termite is based on many open source components available on github:
  • An overlay for the ocaml z3 bindings that enables type-safe creation of SMT formulas: z3overlay
  • LLVM2SMT provides an SMT-encoding of the llvm-ir graph: llvm2smt
  • termite itself.
  
  
• Instalation instructions using opam are available here.
• Comparaison with other termination tools on Ubuntu 64bits

Authors

• Laure Gonnord
• David Monniaux
• Gabriel Radanne

Credits

• Marc Vincenti, for the scripts
• Julien Henry, for the css file