{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:44:19Z","timestamp":1779392659627,"version":"3.53.1"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1999,11,1]],"date-time":"1999-11-01T00:00:00Z","timestamp":941414400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,11,1]],"date-time":"1999-11-01T00:00:00Z","timestamp":941414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1999,11]]},"DOI":"10.1023\/a:1006225515062","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T01:20:41Z","timestamp":1040520041000},"page":"265-298","source":"Crossref","is-referenced-by-count":5,"title":["Formal Verification of a Partial-Order Reduction Technique for Model Checking"],"prefix":"10.1007","volume":"23","author":[{"given":"Ching-Tsun","family":"Chou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"236900_CR1","unstructured":"Boyer, R. S. and Moore, J S.: A Computational Logic, Academic Press, 1979."},{"key":"236900_CR2","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types, Journal of Symbolic Logic\n5 (1940), 56-68.","journal-title":"Journal of Symbolic Logic"},{"key":"236900_CR3","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Filkorn, T. and Jha, S.: Exploiting symmetry in temporal logic model checking, in 5th International Conference on Computer Aided Verification Elounda, Greece, LNCS 697, 1993, pp. 450-462.","DOI":"10.1007\/3-540-56922-7_37"},{"issue":"1","key":"236900_CR4","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P. and Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties, Formal Methods in System Design\n1(1) (1992), 275-288.","journal-title":"Formal Methods in System Design"},{"key":"236900_CR5","unstructured":"Curzon, P. and Wong, W.: A higher-order theory of lists for HOL, presented at 7th Int. Conf. on Higher Order Logic Theorem Proving And Its Applications, Malta, 19-22 September 1994."},{"key":"236900_CR6","doi-asserted-by":"crossref","unstructured":"Emerson, E. A. and Sistla, A. P.: Symmetry and model checking, in 5th International Conference on Computer Aided Verification Elounda, Greece, LNCS 697, 1993, pp. 463-479.","DOI":"10.1007\/3-540-56922-7_38"},{"key":"236900_CR7","volume-title":"Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic","year":"1993","unstructured":"Gordon, M. J. C. and Melham, T. F. (eds.): Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic, Cambridge Univ. Press, Cambridge, 1993."},{"key":"236900_CR8","doi-asserted-by":"crossref","unstructured":"Gordon, M. J. C., Milner, A. J. R. G. and Wadsworth, C. P.: Edinburgh LCF: A Mechanized Logic of Computation, LNCS 78, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"236900_CR9","unstructured":"Holzmann, G. J.: Design and Validation of Computer Protocols, Prentice-Hall, 1991."},{"key":"236900_CR10","unstructured":"Holzmann, G. J. and Peled, D.: An improvement in formal verification, in 7th International Conference on Formal Description Techniques Berne, Switzerland, 1994, pp. 177-194."},{"key":"236900_CR11","doi-asserted-by":"crossref","unstructured":"Holzmann, G. J., Peled, D. and Yannakakis, M.: On nested depth first search, in Second SPIN Workshop, 1996, AMS DIMACS series, to appear 1997, Piscataway, NJ, U.S.A.","DOI":"10.1090\/dimacs\/032\/03"},{"key":"236900_CR12","doi-asserted-by":"crossref","unstructured":"Hungar, H.: Combining model checking and theorem proving to verify parallel processes, in 5th International Conference on Computer Aided Verification Elounda, Greece, LNCS 697, 1993, pp. 154-165.","DOI":"10.1007\/3-540-56922-7_13"},{"key":"236900_CR13","doi-asserted-by":"crossref","unstructured":"Kurshan, R. P.: Computer-Aided Verification of Coordinating Processes, Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"236900_CR14","doi-asserted-by":"crossref","unstructured":"Kurshan, R. P. and Lamport, L.: Verification of a multiplier: 64 bits and beyond, in 5th International Conference on Computer Aided Verification Elounda, Greece, LNCS 697, 1993, pp. 166-179.","DOI":"10.1007\/3-540-56922-7_14"},{"key":"236900_CR15","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF01887206","volume":"1","author":"M. Z. Kwiatkowska","year":"1989","unstructured":"Kwiatkowska, M. Z.: Event fairness and non-interleaving concurrency, Formal Aspects of Computing\n1 (1989), 213-228.","journal-title":"Formal Aspects of Computing"},{"key":"236900_CR16","unstructured":"Lamport, L.: What good is temporal logic, in R. E. A. Mason (ed.), Proceedings of IFIP Congress North-Holland, 1983, pp. 657-668."},{"key":"236900_CR17","unstructured":"Mazurkiewicz, A.: Trace theory, in W. Brauer, W. Reisig, and G. Rozenberg (eds.), Advances in Petri Nets 1986 Bad Honnef, Germany, LCNS 255, Springer, 1987, pp. 279-324."},{"key":"236900_CR18","doi-asserted-by":"crossref","unstructured":"Melham, T. F.: Automating recursive type definitions in higher-order logic, in G. Birtwistle and P. A. Subrahmanyam (eds.), Current Trends in Hardware Verification and Automated Theorem Proving, Springer-Verlag, 1989, pp. 341-386.","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"236900_CR19","doi-asserted-by":"crossref","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking, in 6th International Conference on Computer Aided Verification Stanford, CA, LNCS 818, 1994, pp. 377-390.","DOI":"10.1007\/3-540-58179-0_69"},{"key":"236900_CR20","doi-asserted-by":"crossref","unstructured":"Rajan, S., Shankar, N., and Srivas, M. K.: An integration of model checking with automated proof checking, in 7th International Conference on Computer Aided Verification Li\u00e8ge, Belgium, LNCS 939, 1995, pp. 84-97.","DOI":"10.1007\/3-540-60045-0_42"},{"key":"236900_CR21","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata on infinite objects, in Jan van Leeuwen (ed.), Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics, The MIT Press\/Elsevier, 1990, pp. 133-192.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006225515062.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006225515062\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006225515062.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:24:45Z","timestamp":1749122685000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006225515062"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,11]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1999,11]]}},"alternative-id":["236900"],"URL":"https:\/\/doi.org\/10.1023\/a:1006225515062","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,11]]}}}