Matteo Bertello, Nicola Gigante, Angelo Montanari & Mark Reynolds (2016):
Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau.
In: Subbarao Kambhampati: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016.
IJCAI/AAAI Press,
pp. 950–956.
Available at http://www.ijcai.org/Abstract/16/139.
Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani & Armando Tacchella (2002):
NuSMV 2: An OpenSource Tool for Symbolic Model Checking.
In: Ed Brinksma & Kim Guldstrand Larsen: Computer Aided Verification, 14th International Conference, CAV 2002, Copenhagen, Denmark, July 27-31, 2002, Proceedings,
Lecture Notes in Computer Science 2404.
Springer,
pp. 359–364,
doi:10.1007/3-540-45657-0_29.
Ian T. Foster (1995):
Designing and building parallel programs - concepts and tools for parallel software engineering.
Addison-Wesley.
Oliver Friedmann, Markus Latte & Martin Lange (2010):
A Decision Procedure for CTL* Based on Tableaux and Automata.
In: Jürgen Giesl & Reiner Hähnle: IJCAR 6173.
Springer,
pp. 331–345,
doi:10.1007/978-3-642-14203-1_28.
Nicola Gigante, Angelo Montanari & Mark Reynolds (2017):
A One-Pass Tree-Shaped Tableau for LTL+Past.
In: Thomas Eiter & David Sands: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-21, 7-12 May 2017, Maun, Botswana,
LNCS 46.
Springer,
pp. 456–473.
K. Heljanko, T. Junttila & T. Latvala (2005):
Incremental and complete bounded model checking for full PLTL,
pp. 98–111.
Springer International Publishing,
doi:10.1007/11513988_10.
Ullrich Hustadt & Boris Konev (2003):
TRP++2.0: A Temporal Resolution Prover.
In: Franz Baader: Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings,
Lecture Notes in Computer Science 2741.
Springer,
pp. 274–278,
doi:10.1007/978-3-540-45085-6_21.
Mark Reynolds John McCabe-Dansted (2017):
LTL in the cloud (expanded version).
http://staffhome.ecm.uwa.edu.au/~00061811/papers/parallel.pdf.
Jianwen Li, Geguang Pu, Lijun Zhang, Moshe Y. Vardi & Jifeng He (2014):
Fast LTL Satisfiability Checking by SAT Solvers.
CoRR abs/1401.5677.
Available at http://arxiv.org/abs/1401.5677.
Jianwen Li, Geguang Pu, Lijun Zhang, Yinbo Yao, Moshe Y. Vardi & Jifeng He (2013):
Polsat: A Portfolio LTL Satisfiability Solver.
CoRR abs/1311.1602.
Available at http://arxiv.org/abs/1311.1602.
Jianwen Li, Yinbo Yao, Geguang Pu, Lijun Zhang & Jifeng He (2014):
Aalta: an LTL satisfiability checker over Infinite/Finite traces.
In: Shing-Chi Cheung, Alessandro Orso & Margaret-Anne D. Storey: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16 - 22, 2014.
ACM,
pp. 731–734,
doi:10.1145/2635868.2661669.
Jianwen Li, Shufang Zhu, Geguang Pu & Moshe Y. Vardi (2015):
SAT-Based Explicit LTL Reasoning,
pp. 209–224.
Springer International Publishing,
Cham,
doi:10.1007/978-3-319-26287-1_13.
C. Limongelli, A. Orlandini & V. Poggioni (2003):
A Parallel Computation Technique for Linear Time Logic Tableaux.
In: Tableaux 2003, Position Papers and Tutorials.
Available at http://limongelli.dia.uniroma3.it/papers/tab2003.ps.
S. Malik & L. Zhang (2009):
Boolean satisfiability from theoretical hardness to practical success.
Commun. ACM 52(8),
pp. 76 –82,
doi:10.1145/1536616.1536637.
John C. MCabe-Dansted & Mark Reynolds (2017):
Rewrite rules for CTL*.
Journal of Applied Logic 21,
pp. 24 – 56,
doi:10.1016/j.jal.2016.12.003.
A. Pnueli (1977):
The temporal logic of programs.
In: Proceedings of the Eighteenth Symposium on Foundations of Computer Science,
pp. 46–57,
doi:10.1109/SFCS.1977.32.
Providence, RI.
Mark Reynolds (2016):
A New Rule for LTL Tableaux.
In: Domenico Cantone & Giorgio Delzanno: Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016.,
EPTCS 226,
pp. 287–301,
doi:10.4204/EPTCS.226.20.
Viktor Schuppan & Luthfi Darmawan (2011):
Evaluating LTL Satisfiability Solvers.
In: Tevfik Bultan & Pao-Ann Hsiung: ATVA'11,
Lecture Notes in Computer Science 6996.
Springer,
pp. 397–413,
doi:10.1007/978-3-642-24372-1_28.
Stefan Schwendimann (1998):
A New One-Pass Tableau Calculus for PLTL.
In: Harrie C. M. de Swart: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX '98, Oisterwijk, The Netherlands, May 5-8, 1998, Proceedings,
Lecture Notes in Computer Science 1397.
Springer,
pp. 277–292,
doi:10.1007/3-540-69778-0_28.
Martin Suda & Christoph Weidenbach (2012):
A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance.
In: Bernhard Gramlich, Dale Miller & Uli Sattler: Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings,
Lecture Notes in Computer Science 7364.
Springer,
pp. 537–543,
doi:10.1007/978-3-642-31365-3_42.
O. Tange (2011):
GNU Parallel - The Command-Line Power Tool.
;login: The USENIX Magazine 36(1),
pp. 42–47.
Available at http://www.gnu.org/s/parallel.
eptcs@eptcs.org