Description: Automatic program verification tool for proving temporal properties of programs, such as safety, termination, or properties specified in the logic CTL.
T2 can work directly on C programs.
Developed at: ULEIC/UCL/Microsoft
Contacts: Heidy Khalaaf h.khlaaf@ucl.ac.uk
Mark Brockshmidt mabrocks@microsoft.com
Nir Piterman np183@le.ac.uk
Available at: https://mmjb.github.io/T2/