PV1 Termitecomputes a ranking function for a given program

Internals

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

Links

Last commit date

21 April 2018

Related papers

https://doi.org/10.1145/2737924.2737976 (PLDI 2015)

Related tools

Compared to Loopus, RanK, AProVE,

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.