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