Aalta: an LTL satisfiability checker over Infinite/Finite traces
In Proceedings of the 22nd ACM SIGSOFT International Symposium on
Foundations of Software Engineering (FSE 2014)
, pages 731-734, ACM
, 2014.Downloads: pdf, bibURL: http://doi.acm.org/10.1145/2635868.2661669
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 .