[LiYPZVH14] Aalta: an LTL satisfiability checker over Infinite/Finite traces Li, J.; Yao, Y.; Pu, G.; Zhang, L. and He, J. 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 .