@inproceedings{151810bf28384cba988569ed539f85eb,
title = "Aalta: An LTL satisfiability checker over infinite/finite traces",
abstract = "Linear Temporal Logic (LTL) is widely used nowadays in verification and AI. Checking satisfiability of LTL formulas is a fundamental step in removing possible errors in LTL assertions. We present in this paper Aalta, a new LTL satisfiability checker, which supports satisfiability checking for LTL over both infinite and finite traces. Aalta leverages the power of modern SAT solvers. We have conducted a comprehensive comparison between Aalta and other LTL satisfiability checkers, and the experimental results show that Aalta is very competitive. The tool is available at www.lab205.org/aalta.",
keywords = "Model checking, Satisfiability, Temporal logic",
author = "Jianwen Li and Yinbo Yao and Geguang Pu and Lijun Zhang and Jifeng He",
note = "Publisher Copyright: Copyright 2014 ACM.; 22nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering, FSE 2014 ; Conference date: 16-11-2014 Through 21-11-2014",
year = "2014",
month = nov,
day = "16",
doi = "10.1145/2635868.2661669",
language = "英语",
series = "Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering",
publisher = "Association for Computing Machinery",
pages = "731--734",
booktitle = "22nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering, FSE 2014 - Proceedings",
address = "美国",
}