T2: Temporal Property Verification

TL;DR

T2 is an open-source tool for automatic temporal-logic verification supporting safety and liveness properties, integrating with C code via LLVM, and demonstrating competitive performance.

Contribution

It introduces T2, a versatile, open-source verification tool with decade-long development supporting temporal properties and C integration, advancing automated formal verification.

Findings

T2 effectively verifies temporal properties in C programs.

The tool demonstrates competitive performance in experiments.

Future extensions are discussed for broader applicability.

Abstract

We present the open-source tool T2, the first public release from the TERMINATOR project. T2 has been extended over the past decade to support automatic temporal-logic proving techniques and to handle a general class of user-provided liveness and safety properties. Input can be provided in a native format and in C, via the support of the LLVM compiler framework. We briefly discuss T2's architecture, its underlying techniques, and conclude with an experimental illustration of its competitiveness and directions for future extensions.