PV1 ⊧ Termitecomputes a ranking function for a given program

Internals

Uses LLVM and Clang as frontend
Uses PAGAI as an invariant generator
Uses z3overlay bindings for type-safe connection to Z3
Uses LLVM2SMT to convert a program to a transition relation

Comments

This is admittedly one of the most complex tools on PV1, but it really works fully automatically and does not require/tolerate user input at any stage besides providing the program to work on.

C LLVM

Related tools

Compared to Loopus, RanK, AProVE,

ProVerB specific

Markdown description: view/edit
Reason for this entry: compared to ComPACT
Contained in the ProVerB22 dataset (paper + artefact)

Program
Verification
Book

PV1 ⊧ Termitecomputes a ranking function for a given program

Internals

Comments

Links

Related papers

Related tools

ProVerB specific

ProgramVerificationBook

PV1 ⊧ Termitecomputes a ranking function for a given program

Internals

Comments

Links

Related papers

Related tools

ProVerB specific

Program
Verification
Book