Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
T2 temporal prover

The T2 research project aims to build a high-performance automatic program verification tool for proving termination and liveness properties.  T2 replaces the original TERMINATOR project, which was started in 2005.  See the authors named in the list of publications for an idea of who has contributed to T2 and TERMINATOR over the years. 

T2 is published under the open-source MIT license. A release including methods to prove termination and CTL properties of programs can be downloaded. Development versions can be found on github.

Publications

Faster Temporal Reasoning for Infinite-State Programs
Byron Cook, Heidy Khlaaf, Nir Piterman
FMCAD 2014

Better termination proving through cooperation
Marc Brockschmidt, Byron Cook, Carsten Fuhs
CAV 2013

Reasoning about nondeterminism in programs
Byron Cook and Eric Koskinen
PLDI 2013

Ramsey vs. lexicographic termination proving
Byron Cook, Abigail See, and Florian Zuleger
TACAS 2013

Ranking function synthesis for bit-vector relations
Byron Cook, Daniel Kroening, Philipp Rummer, Christoph Wintersteiger
Formal Methods in System Design, 2013

Proving termination of nonlinear command sequences
Domagoj Babic, Byron Cook, Alan J. Hu, Zvonimir Rakamaric
Formal Aspects of Computing (special issue from SEFM), 2013

Temporal property verification as a program analysis task (extended version)
Byron Cook, Eric Koskinen, Moshe Vardi
Formal Methods in System Design (special issue from CAV), 2012

Proving program termination (Review article)
Byron Cook, Andreas Podelski, Andrey Rybalchenko
Communications of the ACM, Volume 54 Issue 5, May 2011

Temporal property verification as a program analysis task
Byron Cook, Eric Koskinen, Moshe Vardi
CAV'11 [International Conference on Computer-Aided Verification] (Snowbird)

Making prophecies with decision predicates
Byron Cook and Eric Koskinen
POPL'11 [Symposium on Principles of Programming Languages] (Austin)

Proving stabilization of biological systems
Byron Cook, Jasmin Fisher, Elzbieta Krepska, Nir Piterman
VMCAI'11 [Verification, model checking, and abstract interpretation] (Austin)

Ranking function synthesis for bit-vector relations
Byron Cook, Daniel Kroening, Philipp Rummer, and Christoph Wintersteiger
TACAS'10 [Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems]

Summarization for termination: No return!
Byron Cook, Andreas Podelski, Andrey Rybalchenko
FMSD (2009) 35:369-387

Proving that non-blocking algorithms don't block
Alexey Gotsman, Byron Cook, Matthew Parkinson, and Viktor Vafeiadis
POPL'09 [Symposium on Principles of Programming Languages] (Savannah)

Proving conditional termination
Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, and Mooly Sagiv
CAV'08 [International Conference on Computer-Aided Verification] (Princeton)

Ranking abstractions
Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang
ESOP'08 [European Symposium on Programming] (Budapest)

Proving thread termination
Byron Cook, Andreas Podelski, and Andrey Rybalchenko
PLDI'07 [Conference on Programming Language Design and Implementation] (San Diego)

Proving termination by divergence
Domagoj Babic, Byron Cook, Alan Hu, Zvonimir Rakamaric
SEFM'07 [ International Conference on Software Engineering and Formal Methods] (London)

Arithmetic strengthening for shape analysis
Stephen Magill, Josh Berdine, Edmund Clarke, and Byron Cook.
SAS'07 [International Static Analysis Symposium] (Denmark)

Proving that programs eventually do something good
Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Vardi
POPL'07 [Symposium on Principles of Programming Languages] (Nice)

Variance analyses from invariance analyses
Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, and Peter O'Hearn
POPL'07 [Symposium on Principles of Programming Languages] (Nice)

Automatic termination proofs for programs with shape-shifting heaps
Josh Berdine, Byron Cook, Dino Distefano, and Peter O'Hearn
CAV'06 [International Conference on Computer-Aided Verification] (Seattle)

Terminator: Beyond safety (short tool description paper)
Byron Cook, Andreas Podelski, and Andrey Rybalchenko
CAV'06 [International Conference on Computer-Aided Verification] (Seattle)

Termination proofs for systems code
Byron Cook, Andreas Podelski, and Andrey Rybalchenko
PLDI'06 [Conference on Programming Language Design and Implementation] (Ottawa)

Abstraction refinement for termination
Byron Cook, Andreas Podelski, Andrey Rybalchenko
SAS'05 [International Static Analysis Symposium] (London)

Sources

Press