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

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

Application domain/field

• Temporal properties
• Computation tree logic (CTL)
• Linear temporal logic (LTL)
• Termination
• Safety verification

Expected input

• Program
• Indicate whether to check/verify a temporal property, termination or safety.

Format:

• Program: T2's own syntax, .t2 file. This syntax can automatically be extracted from LLVM thereby providing support for several programming languages, e.g. C and C++.
• Temporal property: If checking a temporal property, then the property is passed as a string argument when calling T2
• Termination/safety checking: If checking for (non-)termination or safety, then the user should pass either -termination or -safety where indicates the location.

Expected output

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

Internals

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