Please use this identifier to cite or link to this item:
Title: T2: Temporal Property Verification
Authors: Brockschmidt, Mark
Cook, Byron
Ishtiaq, Samin
Khlaaf, Heidy
Piterman, Nir
First Published: 9-Apr-2016
Presented at: 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2-8 April 2016, Eindhoven, The Netherlands
Start Date: 2-Apr-2016
End Date: 8-Apr-2016
Publisher: Springer-Verlag
Citation: Lecture Notes in Computer Science, 2016, 9636, pp 387-393
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.
DOI Link: 10.1007/978-3-662-49674-9_22
ISSN: 0302-9743
ISBN: 9783662496732
Version: Post-print
Type: Conference Paper
Rights: Copyright © Springer Verlag, 2015. This version is an open-access article distributed under the terms of the Creative Commons Attribution-Non Commercial-No Derivatives License ( ), which permits use and distribution in any medium, provided the original work is properly cited, the use is non-commercial and no modifications or adaptations are made.
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
paper_107.pdfPost-review (final submitted)398.5 kBUnknownView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.