{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:25Z","timestamp":1761611125043},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2004,3,1]],"date-time":"2004-03-01T00:00:00Z","timestamp":1078099200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["STTT"],"published-print":{"date-parts":[[2004,3]]},"DOI":"10.1007\/s10009-003-0121-x","type":"journal-article","created":{"date-parts":[[2004,3,19]],"date-time":"2004-03-19T18:53:20Z","timestamp":1079722400000},"page":"185-204","source":"Crossref","is-referenced-by-count":46,"title":["Efficient reduction of finite state model checking to reachability analysis"],"prefix":"10.1007","volume":"5","author":[{"given":"Viktor","family":"Schuppan","sequence":"first","affiliation":[]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,3,1]]},"reference":[{"key":"121_CR1","doi-asserted-by":"crossref","unstructured":"Baumgartner J, K\u00fchlmann A, Abraham J (2002) Property checking via structural analysis. In: Brinksma E, Larsen K (eds) Proceedings of the 14th international conference on computer aided verification (CAV 2002), Copenhagen, Denmark, 27\u201331 July 2002. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 151\u2013165","DOI":"10.1007\/3-540-45657-0_12"},{"key":"121_CR2","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E, Fujita M, Zhu Y (1999a) Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the 36th ACM\/IEEE conference on design automation (DAC\u201999), New Orleans, 21\u201325 June 1999, pp 317\u2013320. ACM Press, New York","DOI":"10.1145\/309847.309942"},{"key":"121_CR3","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E, Zhu Y (1999b) Symbolic model checking without BDDs. In: Cleaveland R (ed) Proceedings of the 5th international conference on tools and algorithms for construction and analysis of systems (TACAS \u201999), Amsterdam, 22\u201328 March 1999. Lecture notes in computer science, vol 1579. Springer, Berlin Heidelberg New York, pp 193\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"key":"121_CR4","doi-asserted-by":"crossref","unstructured":"Biere A, Clarke E, Zhu Y (1999c) Multiple state and single state tableaux for combining local and global model checking. In: Olderog ER, Steffen B (eds) Correct system design, recent insight and advances. Lecture notes in computer science, vol 1710. Springer, Berlin Heidelberg New York, pp 163\u2013179","DOI":"10.1007\/3-540-48092-7_8"},{"key":"121_CR5","doi-asserted-by":"crossref","unstructured":"Biere A, Artho C, Schuppan V (2002) Liveness checking as safety checking. In: Cleaveland R, Garavel H (eds) Proceedings of the 7th international ERCIM workshop on formal methods for industrial critical systems (FMICS\u201902), M\u00e1laga, Spain, 12\u201313 July 2002. Electronic notes in theoretical computer science, 66(2). Elsevier, Amsterdam","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"121_CR6","doi-asserted-by":"crossref","unstructured":"Browne M, Clarke E, Grumberg O (1988) Characterizing finite Kripke structures in propositional logic. Theor Comput Sci 59(1\u20132):115\u2013131","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"121_CR7","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"Bryant","year":"1986","unstructured":"Bryant R (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691","journal-title":"IEEE Trans Comput"},{"key":"121_CR8","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke E, Giunchiglia F, Roveri M (1999) NuSMV: a new symbolic model verifier. In: Halbwachs and Peled [15], pp 495\u2013499","DOI":"10.1007\/3-540-48683-6_44"},{"key":"121_CR9","doi-asserted-by":"crossref","unstructured":"Clarke E, Emerson A (1982) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen D (ed) Proceedings of the workshop on logic of programs, Yorktown Heights, NY, May 1981, Lecture notes in computer science, vol 131. Springer, Berlin Heidelberg New York, pp 52\u201371","DOI":"10.1007\/BFb0025774"},{"key":"121_CR10","unstructured":"Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge, MA"},{"key":"121_CR11","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"Courcoubetis","year":"1992","unstructured":"Courcoubetis C, Vardi M, Wolper P, Yannakakis M (1992) Memory efficient algorithms for the verification of temporal properties. Formal Meth Sys Des 1:275\u2013288","journal-title":"Formal Meth Sys Des"},{"key":"121_CR12","doi-asserted-by":"crossref","unstructured":"Emerson A (1999) Temporal and modal logic. In: van Leeuwen J (ed) Handbook of theoretical computer science: Volume B. Formal methods and semantics, pp 995\u20131072. North-Holland, Amsterdam","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"121_CR13","doi-asserted-by":"crossref","unstructured":"Gerth R, Peled D, Vardi M, Wolper P (1996) Simple on-the-fly automatic verification of linear temporal logic. In: Dembinski P, Sredniawa M (eds) Proceedings of the 15th IFIP WG6.1 international symposium on protocol specification, testing and verification, Warsaw, Poland, June 1995. IFIP conference proceedings, 38:3\u201318. Chapman & Hall, London","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"121_CR14","doi-asserted-by":"crossref","unstructured":"Giannakopoulou D, Havelund K (2001) Automata-based verification of temporal properties on running programs. In: Proceedings of the 16th IEEE international conference on automated software engineering (ASE 2001), 26\u201329 November 2001, Coronado Island, San Diego, CA, pp 412\u2013416. IEEE Press, New York","DOI":"10.1109\/ASE.2001.989841"},{"key":"121_CR15","doi-asserted-by":"crossref","unstructured":"Halbwachs N, Peled D (eds) (1999) Proceedings of the 11th international conference on computer aided verification (CAV \u201999), Trento, Italy, 6\u201310 July 1999. Lecture notes in computer science, vol 1633. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-48683-6"},{"key":"121_CR16","doi-asserted-by":"crossref","unstructured":"Halbwachs N, Lagnier F, Raymond P (1994) Synchronous observers and the verification of reactive systems. In: Nivat M, Rattray C, Rus T, Scollo G (eds) Proceedings of the 3rd international conference on algebraic methodology and software technology (AMAST \u201993), University of Twente, Enschede, The Netherlands, 21\u201325 June 1993. Workshops in computing. Springer, Berlin Heidelberg New York, pp 83\u201396","DOI":"10.1007\/978-1-4471-3227-1_8"},{"key":"121_CR17","doi-asserted-by":"crossref","unstructured":"Havelund K, Ro\u015fu G (2001) Monitoring Java programs with Java PathExplorer. In: Havelund K, Ro\u015fu G (eds) Proceedings of the 1st international workshop on runtime verification (RV\u201901), Paris, France, 23 July 2001. Electronic notes in theoretical computer science, 55(2). Elsevier, 2001.","DOI":"10.1016\/S1571-0661(04)00253-1"},{"key":"121_CR18","doi-asserted-by":"crossref","unstructured":"Havelund K, Ro\u015fu G (2002) Synthesizing monitors for safety properties. In: Katoen J-P, Stevens P (eds) Proceedings of the 8th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2002), Grenoble, France, 8\u201312 April 2002. Lecture notes in computer science, vol 2280. Springer, Berlin Heidelberg New York, pp 342\u2013356","DOI":"10.1007\/3-540-46002-0_24"},{"key":"121_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger T, Kupferman O, Qadeer S (1998) From pre-historic to post-modern symbolic model checking. In: Hu A, Vardi M (eds) Proceedings of the 10th international conference on computer aided verification (CAV \u201998), Vancouver, BC, Canada, 28 June\u20132 July 1998. Lecture notes in computer science, vol 1427. Springer, Berlin Heidelberg New York, pp 195\u2013206","DOI":"10.1007\/BFb0028745"},{"key":"121_CR20","doi-asserted-by":"crossref","unstructured":"Iwashita H, Nakata T, Hirose F (1996) CTL model checking based on forward state traversal. In: Proceedings of the 1996 IEEE\/ACM international conference on computer-aided design, San Jose, CA, 10\u201314 November 1996, pp 82\u201387. IEEE Press, New York","DOI":"10.1109\/ICCAD.1996.569084"},{"key":"121_CR21","doi-asserted-by":"crossref","unstructured":"Jagadeesan L, Puchol C, von Olnhausen J (1995) Safety property verification of ESTEREL programs and applications to telecommunications software. In: Wolper P (ed) Proceedings of the 7th international conference on computer aided verification, Li\u00e8ge, Belgium, 3\u20135 July 1995. Lecture notes in computer science, vol 939. Springer, Berlin Heidelberg New York, pp 127\u2013140","DOI":"10.1007\/3-540-60045-0_45"},{"key":"121_CR22","doi-asserted-by":"crossref","unstructured":"Kr\u00f6ning D, Strichman O (2003) Efficient computation of recurrence diameters. In: Zuck L, Attie P, Cortesi A, Mukhopadhyay S (eds) Proceedings of the 4th international conference on verification, model checking, and abstract interpretation (VMCAI 2003), New York, 9\u201311 January 2002. Lecture notes in computer science, vol 2575. Springer, Berlin Heidelberg New York, pp 298\u2013309","DOI":"10.1007\/3-540-36384-X_24"},{"key":"121_CR23","doi-asserted-by":"crossref","unstructured":"Kupferman O, Vardi M (1999) Model checking of safety properties. In: Halbwachs and Peled [15], pp 172\u2013183","DOI":"10.1007\/3-540-48683-6_17"},{"key":"121_CR24","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"Lamport","year":"1977","unstructured":"Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng 3(2):125\u2013143","journal-title":"IEEE Trans Softw Eng"},{"key":"121_CR25","unstructured":"McMillan K Cadence SMV. http:\/\/www-cad.eecs.berkeley.edu\/ kenmcmil\/smv."},{"key":"121_CR26","first-page":"an","volume":"checking","author":"McMillan","year":"1993","unstructured":"McMillan K (1993) Symbolic model checking: an approach to the state explosion problem. Kluwer, Dordrecht","journal-title":"Symbolic model"},{"key":"121_CR27","doi-asserted-by":"crossref","unstructured":"Niermann T, Patel J (1991) HITEC: A test generation package for sequential circuits. In: Proceedings of the European conference on design automation, Amsterdam, 25\u201328 February 1991, pp 214\u2013218. IEEE Press, New York","DOI":"10.1109\/EDAC.1991.206393"},{"key":"121_CR28","doi-asserted-by":"crossref","unstructured":"Peled D (2001) Software reliability methods. Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-1-4757-3540-6"},{"key":"121_CR29","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s001650300005","volume":"14","author":"Schuppan","year":"2003","unstructured":"Schuppan V, Biere A (2003) Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV. Formal Asp Comput 14(3):267\u2013280","journal-title":"Formal Asp Comput"},{"key":"121_CR30","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"Seger","year":"1995","unstructured":"Seger C-J, Bryant R (1995) Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Meth Sys Des 6(2):147\u2013189","journal-title":"Formal Meth Sys Des"},{"key":"121_CR31","doi-asserted-by":"crossref","unstructured":"Sheeran M, Singh S, St\u00e5lmarck G (2000) Checking safety properties using induction and a SAT-solver. In: Hunt Jr W, Johnson S (eds) Proceedings of the 3rd international conference on formal methods in computer-aided design (FMCAD 2000), Austin, TX, 1\u20133 November 2000. Lecture notes in computer science, vol 1954. Springer, Berlin Heidelberg New York, pp 108\u2013125","DOI":"10.1007\/3-540-40922-X_8"},{"key":"121_CR32","unstructured":"Somenzi F Wring 1.1.0. ftp:\/\/vlsi.colorado.edu\/pub\/Wring-1.1.0.tar.gz."},{"key":"121_CR33","doi-asserted-by":"crossref","unstructured":"Somenzi F, Bloem R (2000) Efficient Buchi automata from ltl formulae. In: Emerson A, Sistla P (eds) Proceedings of the 12th international conference on computer aided verification (CAV 2000), Chicago, 15\u201319 July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 248\u2013263","DOI":"10.1007\/10722167_21"},{"key":"121_CR34","unstructured":"The VIS Group (1996) VIS: a system for verification and synthesis. In: Alur R, Henzinger T (eds) Proceedings of the 8th international conference on computer aided verification (CAV \u201996), New Brunswick, NJ, 31 July\u20133 August 1996. Lecture notes in computer science, vol 1102. Springer, Berlin Heidelberg New York, pp 428\u2013432"},{"key":"121_CR35","unstructured":"Yang B. SMV models. http:\/\/www.cs.cmu.edu\/ bwolen\/software\/smv-models\/."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0121-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-003-0121-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0121-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0121-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,31]],"date-time":"2020-03-31T17:56:09Z","timestamp":1585677369000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-003-0121-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,3]]},"references-count":35,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2004,3]]}},"alternative-id":["121"],"URL":"https:\/\/doi.org\/10.1007\/s10009-003-0121-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,3]]}}}