PV3 T2can check termination or user-specified properties of LLVM code

Verifier for temporal properties, (non)termination and safety of programs

Application domain/field

Expected input


Expected output

Whether the proof (either safety, termination or temporal) succeeded.


Users can use T2 to (dis)prove LTL, CTL, Fair-CTL and CTL* specifications. Uses Z3.
CTL LTL Termination


Repository: https://github.com/mmjb/T2

Related papers

Last publication date

11 July 2017

Related tools

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.