kirancodes.me
To Proof Maintenance & Beyond!
FSE 2014

Aalta: an LTL satisfiability checker over Infinite/Finite traces

Jianwen Li, Yinbo Yao, Geguang Pu, Lijun Zhang, Jifeng He

PDFDOI 10.1145/2635868.2661669dblp

Abstract

Linear Temporal Logic (LTL) is been 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.

BibTeX
@inproceedings{Li-al:FSE14,
  author    = {Jianwen Li and
               Yinbo Yao and
               Geguang Pu and
               Lijun Zhang and
               Jifeng He},
  title     = {Aalta: an {LTL} satisfiability checker over {Infinite/Finite} traces},
  booktitle = {FSE},
  pages     = {731--734},
  publisher = {{ACM}},
  year      = {2014},
}

Related papers