{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:27:58Z","timestamp":1746289678801},"publisher-location":"Berlin, Heidelberg","reference-count":70,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642243714"},{"type":"electronic","value":"9783642243721"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-24372-1_28","type":"book-chapter","created":{"date-parts":[[2011,9,29]],"date-time":"2011-09-29T09:41:14Z","timestamp":1317289274000},"page":"397-413","source":"Crossref","is-referenced-by-count":32,"title":["Evaluating LTL Satisfiability Solvers"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Schuppan","sequence":"first","affiliation":[]},{"given":"Luthfi","family":"Darmawan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","unstructured":"http:\/\/www.antichains.be\/alaska\/"},{"key":"28_CR2","unstructured":"http:\/\/www.lwb.unibe.ch\/index.html"},{"key":"28_CR3","unstructured":"http:\/\/nusmv.fbk.eu\/"},{"key":"28_CR4","unstructured":"http:\/\/users.cecs.anu.edu.au\/~rpg\/PLTLProvers\/"},{"key":"28_CR5","unstructured":"http:\/\/www.csc.liv.ac.uk\/~konev\/software\/trp++\/"},{"key":"28_CR6","unstructured":"http:\/\/www.csc.liv.ac.uk\/~michel\/software\/tspass\/"},{"key":"28_CR7","unstructured":"http:\/\/www.schuppan.de\/viktor\/atva11\/"},{"key":"28_CR8","unstructured":"http:\/\/www.kenmcmil.com\/smv.html"},{"key":"28_CR9","unstructured":"http:\/\/minisat.se\/"},{"key":"28_CR10","unstructured":"http:\/\/www.antichains.be\/acacia\/"},{"key":"28_CR11","unstructured":"http:\/\/www.iaik.tugraz.at\/content\/research\/design_verification\/anzu\/"},{"key":"28_CR12","unstructured":"http:\/\/shemesh.larc.nasa.gov\/people\/kyr\/benchmarking_scripts\/benchmarking_scripts.html"},{"key":"28_CR13","unstructured":"http:\/\/www.csc.liv.ac.uk\/~ullrich\/TRP\/"},{"key":"28_CR14","unstructured":"http:\/\/www.cril.univ-artois.fr\/PB10\/"},{"key":"28_CR15","unstructured":"Abate, P., Gor\u00e9, R.: The Tableau Workbench. In: M4M (2007)"},{"key":"28_CR16","unstructured":"Beer, I., et al.: Efficient Detection of Vacuity in Temporal Model Checking. FMSD\u00a018(2) (2001)"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Behdenna, A., Dixon, C., Fisher, M.: Deductive Verification of Simple Foraging Robotic Behaviours. Int. J. of Intelligent Comput. and Cybernetics\u00a02(4) (2009)","DOI":"10.1108\/17563780911005818"},{"key":"28_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-540-24605-3_34","volume-title":"Theory and Applications of Satisfiability Testing","author":"D. Berre Le","year":"2004","unstructured":"Le Berre, D., Simon, L.: The Essentials of the SAT 2003 Competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 452\u2013467. Springer, Heidelberg (2004)"},{"key":"28_CR19","unstructured":"Le Berre, D., et al.: The SAT 2009 competition results: does theory meet practice (presentation). In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584. Springer, Heidelberg (2009)"},{"key":"28_CR20","unstructured":"Biere, A., Claessen, K.: Hardware Model Checking Competition (presentation). In: Hardware Verification Workshop 2010, Edinburgh, UK (2010)"},{"key":"28_CR21","unstructured":"Biere, A., Jussila, T.: Benchmark Tool Run, http:\/\/fmv.jku.at\/run\/"},{"key":"28_CR22","volume-title":"Handbook of Satisfiability","author":"A. Biere","year":"2009","unstructured":"Biere, A., et al.: Handbook of Satisfiability. IOS Press, Amsterdam (2009)"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"Bloem, R., et al.: Automatic hardware synthesis from specifications: a case study. In: DATE (2007)","DOI":"10.1109\/DATE.2007.364456"},{"key":"28_CR24","series-title":"ENTCS","volume-title":"COCV","author":"R. Bloem","year":"2007","unstructured":"Bloem, R., et al.: Specify, Compile, Run: Hardware from PSL. In: COCV. ENTCS, vol.\u00a0190(4). Elsevier, Amsterdam (2007)"},{"key":"28_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-540-73368-3_53","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2007","unstructured":"Cimatti, A., et al.: Boolean Abstraction for Temporal Logic Satisfiability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 532\u2013546. Springer, Heidelberg (2007)"},{"key":"28_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"28_CR27","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Hamaguchi, K.: Another Look at LTL Model Checking. FMSD\u00a010(1) (1997)","DOI":"10.1023\/A:1008615614281"},{"key":"28_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"M. Daniele","year":"1999","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.: Improved Automata Generation for Linear Temporal Logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"key":"28_CR29","doi-asserted-by":"crossref","unstructured":"Emerson, E.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, vol. B: Formal Models and Sematics (B) (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"28_CR30","unstructured":"Emerson, E., Lei, C.: Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract). In: LICS (1986)"},{"key":"28_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-02658-4_22","volume-title":"Computer Aided Verification","author":"E. Filiot","year":"2009","unstructured":"Filiot, E., Jin, N., Raskin, J.: An Antichain Algorithm for LTL Realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 263\u2013277. Springer, Heidelberg (2009)"},{"key":"28_CR32","doi-asserted-by":"crossref","unstructured":"Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Trans. Comput. Log. 2(1) (2001)","DOI":"10.1145\/371282.371311"},{"key":"28_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-01702-5_7","volume-title":"Hardware and Software: Verification and Testing","author":"D. Fisman","year":"2009","unstructured":"Fisman, D., et al.: A Framework for Inherent Vacuity. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol.\u00a05394, pp. 7\u201322. Springer, Heidelberg (2009)"},{"key":"28_CR34","doi-asserted-by":"crossref","unstructured":"Gomes, C., Selman, B.: Algorithm portfolios. Artif. Intell.\u00a0126(1-2) (2001)","DOI":"10.1016\/S0004-3702(00)00081-3"},{"key":"28_CR35","doi-asserted-by":"crossref","unstructured":"Goranko, V., Kyrilov, A., Shkatov, D.: Tableau Tool for Testing Satisfiability in LTL: Implementation and Experimental Analysis. In: M4M (2009)","DOI":"10.1016\/j.entcs.2010.04.009"},{"key":"28_CR36","unstructured":"Gor\u00e9, R.: Personal Communication (2010)"},{"key":"28_CR37","doi-asserted-by":"crossref","unstructured":"Gor\u00e9, R., Widmann, F.: An Experimental Comparison of Theorem Provers for CTL. In: CLoDeM (2010)","DOI":"10.1109\/TIME.2011.16"},{"key":"28_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/978-3-642-02959-2_32","volume-title":"Automated Deduction \u2013 CADE-22","author":"R. Gor\u00e9","year":"2009","unstructured":"Gor\u00e9, R., Widmann, F.: An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 437\u2013452. Springer, Heidelberg (2009)"},{"key":"28_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11513988_10","volume-title":"Computer Aided Verification","author":"K. Heljanko","year":"2005","unstructured":"Heljanko, K., Junttila, T., Latvala, T.: Incremental and Complete Bounded Model Checking for Full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 98\u2013111. Springer, Heidelberg (2005)"},{"key":"28_CR40","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Kupferman, O., Qadeer, S.: From Pre-Historic to Post-Modern Symbolic Model Checking. FMSD\u00a023(3) (2003)","DOI":"10.1023\/A:1026228213080"},{"key":"28_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/3-540-59338-1_44","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"A. Heuerding","year":"1995","unstructured":"Heuerding, A., et al.: Propositional Logics on the Computer. In: Baumgartner, P., Posegga, J., H\u00e4hnle, R. (eds.) TABLEAUX 1995. LNCS, vol.\u00a0918, pp. 310\u2013323. Springer, Heidelberg (1995)"},{"key":"28_CR42","unstructured":"Hirsch, B., Hustadt, U.: Translating PLTL into WS1S: Application Description. In: M4M (2001)"},{"key":"28_CR43","doi-asserted-by":"crossref","unstructured":"Huberman, B., Lukose, R., Hogg, T.: An Economics Approach to Hard Computational Problems. Science\u00a0275(5296) (1997)","DOI":"10.1126\/science.275.5296.51"},{"key":"28_CR44","unstructured":"Hustadt, U., Konev, B.: TRP++: A temporal resolution prover. In: Collegium Logicum, vol.\u00a08. Kurt G\u00f6del Society (2004)"},{"key":"28_CR45","unstructured":"Hustadt, U., Schmidt, R.A.: Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers. Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics. Dipartimento, di Ingegneria dell\u2019Informazione, Unversit\u00e1 degli Studi di Siena (2001)"},{"key":"28_CR46","volume-title":"KR","author":"U. Hustadt","year":"2002","unstructured":"Hustadt, U., Schmidt, R.A.: Scientific Benchmarking with Temporal Logic Decision Procedures. In: KR. Morgan Kaufmann, San Francisco (2002)"},{"key":"28_CR47","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-25984-8_23","volume-title":"Automated Reasoning","author":"U. Hustadt","year":"2004","unstructured":"Hustadt, U., et al.: TeMP: A Temporal Monodic Prover. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 326\u2013330. Springer, Heidelberg (2004)"},{"key":"28_CR48","unstructured":"Janssen, G.: Logics for Digital Circuit Verification: Theory, Algorithms, and Applications. PhD thesis. Technische Universiteit Eindhoven (1999)"},{"key":"28_CR49","volume-title":"IJCAI","author":"K. Leyton-Brown","year":"2003","unstructured":"Leyton-Brown, K., et al.: A Portfolio Approach to Algorithm Selection. In: IJCAI. Morgan Kaufmann, San Francisco (2003)"},{"key":"28_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-642-02959-2_21","volume-title":"Automated Deduction \u2013 CADE-22","author":"M. Ludwig","year":"2009","unstructured":"Ludwig, M., Hustadt, U.: Fair Derivations in Monodic Temporal Reasoning. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 261\u2013276. Springer, Heidelberg (2009)"},{"key":"28_CR51","doi-asserted-by":"crossref","unstructured":"Ludwig, M., Hustadt, U.: Implementing a fair monodic temporal logic prover. AI Commun.\u00a023(2-3) (2010)","DOI":"10.3233\/AIC-2010-0457"},{"key":"28_CR52","doi-asserted-by":"crossref","unstructured":"Ludwig, M., Hustadt, U.: Resolution-Based Model Construction for PLTL. In: TIME (2009)","DOI":"10.1109\/TIME.2009.11"},{"key":"28_CR53","doi-asserted-by":"crossref","unstructured":"de Moura, L.: SAL: Tutorial (2004)","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"28_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2004","unstructured":"de Moura, L., et al.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 496\u2013500. Springer, Heidelberg (2004)"},{"key":"28_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-14186-7_18","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"M. Nikoli\u0107","year":"2010","unstructured":"Nikoli\u0107, M.: Statistical Methodology for Comparison of SAT Solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 209\u2013222. Springer, Heidelberg (2010)"},{"key":"28_CR56","doi-asserted-by":"crossref","unstructured":"Pill, I., et al.: Formal analysis of hardware requirements. In: DAC (2006)","DOI":"10.1145\/1146909.1147119"},{"key":"28_CR57","unstructured":"Prosyd, http:\/\/www.prosyd.org\/"},{"key":"28_CR58","doi-asserted-by":"crossref","unstructured":"Pulina, L., Tacchella, A.: A self-adaptive multi-engine solver for quantified Boolean formulas. Constraints 14(1) (2009)","DOI":"10.1007\/s10601-008-9051-2"},{"key":"28_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-642-21437-0_31","volume-title":"FM 2011: Formal Methods","author":"K. Rozier","year":"2011","unstructured":"Rozier, K., Vardi, M.: A Multi-Encoding Approach for LTL Symbolic Satisfiability Checking. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 417\u2013431. Springer, Heidelberg (2011)"},{"key":"28_CR60","doi-asserted-by":"crossref","unstructured":"Rozier, K., Vardi, M.: LTL Satisfiability Checking. STTT 12(2) (2010)","DOI":"10.1007\/s10009-010-0140-3"},{"key":"28_CR61","doi-asserted-by":"crossref","unstructured":"Schuppan, V.: Towards a notion of unsatisfiable and unrealizable cores for LTL. Sci. Comput. Program (2010) (in Press), doi:10.1016\/j.scico.2010.11.004","DOI":"10.1016\/j.scico.2010.11.004"},{"key":"28_CR62","doi-asserted-by":"crossref","unstructured":"Schuppan, V., Darmawan, L.: Evaluating LTL Satisfiability Solvers (full version) (2011), http:\/\/www.schuppan.de\/viktor\/VSchuppanLDarmawan-ATVA-2011-full.pdf","DOI":"10.1007\/978-3-642-24372-1_28"},{"key":"28_CR63","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/3-540-69778-0_28","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S. Schwendimann","year":"1998","unstructured":"Schwendimann, S.: A New One-Pass Tableau Calculus for PLTL. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 277\u2013292. Springer, Heidelberg (1998)"},{"key":"28_CR64","unstructured":"Simon, L., Le Berre, D.: Some Results and Lessons from the SAT Competitions (invited talk, slides only). In: Second International Workshop on Constraint Propagation and Implementation, Sitges, Spain (October 1, 2005)"},{"key":"28_CR65","unstructured":"StatSoft, Inc. Electronic Statistics Textbook. StatSoft, Tulsa, OK, USA, http:\/\/www.statsoft.com\/textbook\/"},{"key":"28_CR66","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Suttner, C.: Evaluating general purpose automated theorem proving systems. Artif. Intell. 131(1-2) (2001)","DOI":"10.1016\/S0004-3702(01)00113-8"},{"key":"28_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Computer Aided Verification","author":"The VIS Group","year":"1996","unstructured":"The VIS Group: VIS: A System for Verification and Synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"key":"28_CR68","unstructured":"Wolper, P.: The Tableau Method for Temporal Logic: An Overview. Logique et Analyse 28(110-111) (1985)"},{"key":"28_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-540-78800-3_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Wulf De","year":"2008","unstructured":"De Wulf, M., et al.: Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 63\u201377. Springer, Heidelberg (2008)"},{"key":"28_CR70","doi-asserted-by":"crossref","unstructured":"Xu, L., et al.: SATzilla: Portfolio-based Algorithm Selection for SAT. JAIR 32 (2008)","DOI":"10.1613\/jair.2490"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24372-1_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,25]],"date-time":"2020-06-25T06:09:40Z","timestamp":1593065380000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24372-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642243714","9783642243721"],"references-count":70,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24372-1_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}