T2：时态性质验证
计算机科学中的逻辑
2016-01-07 v2
摘要
我们提出开源工具T2，即TERMINATOR项目的首次公开发布。T2在过去十年中经过扩展，支持自动时态逻辑证明技术，并处理一类通用的用户提供的活性与安全性性质。可通过LLVM编译器框架的支持以原生格式和C语言提供输入。我们简要讨论T2的架构、其底层技术，并以实验展示其竞争力及未来扩展方向作结。
引用
@article{arxiv.1512.08689,
title = {T2: Temporal Property Verification},
author = {Marc Brockschmidt and Byron Cook and Samin Ishtiaq and Heidy Khlaaf and Nir Piterman},
journal= {arXiv preprint arXiv:1512.08689},
year = {2016}
}
备注
Full version of TACAS'16 tool paper