University of Leicester
Browse
1512.08689v2.pdf (633.97 kB)

T2: Temporal Property Verification

Download (633.97 kB)
report
posted on 2016-05-18, 14:45 authored by Mark Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman
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.

History

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Science

Version

  • NA (Not Applicable or Unknown)

Copyright date

2015

Available date

2016-05-18

Publisher version

http://link.springer.com/chapter/10.1007/978-3-662-49674-9_22

Notes

This is an extended version of a paper presented at the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems and published in the Proceedings as Brockschmidt, M., Cook, B. et. al., T2: Temporal Property Verification, Lecture Notes in Computer Science, 2016, 9636, pp 387-393.

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    No categories selected

    Keywords

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC