{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:31:38Z","timestamp":1754487098110},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540610427"},{"type":"electronic","value":"9783540498742"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61042-1_48","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:11:22Z","timestamp":1330290682000},"page":"241-257","source":"Crossref","is-referenced-by-count":21,"title":["Formal verification of a partial-order reduction technique for model checking"],"prefix":"10.1007","author":[{"given":"Ching -Tsun","family":"Chou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"15_CR1","unstructured":"Robert S. Boyer and J. Strother Moore, A Computational Logic, Academic Press, 1979."},{"key":"15_CR2","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Alonzo Church, \u201cA Formulation of the Simple Theory of Types\u201d, in Journal of Symbolic Logic, Vol. 5, pp. 56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"key":"15_CR3","first-page":"450","volume":"697","author":"E.M. Clarke","year":"1993","unstructured":"E.M. Clarke, T. Filkorn, S. Jha, Exploiting Symmetry in Temporal Logic Model Checking, 5th International Conference on Computer Aided Verification, Elounda, Greece, June 1993, LNCS 697, 450\u2013462.","journal-title":"LNCS"},{"key":"15_CR4","first-page":"463","volume":"697","author":"E.A. Emerson","year":"1993","unstructured":"E.A. Emerson, A.P. Sistla, Symmetry and Model Checking, 5th International Conference on Computer Aided Verification, Elounda, Greece, June 1993, LNCS 697, 463\u2013479.","journal-title":"LNCS"},{"key":"15_CR5","unstructured":"Michael J.C. Gordon and Thomas F. Melham (Ed.), Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic, Cambridge University Press, 1993."},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"M.J.C. Gordon, A.J.R.G. Milner, and C.P. Wadsworth, Edinburgh LCF: A Mechanized Logic of Computation, Lecture Notes in Computer Science 78, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"15_CR7","unstructured":"G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991."},{"key":"15_CR8","unstructured":"G.J. Holzmann, D. Peled, An Improvement in Formal Verification, 7th International Conference on Formal Description Techniques, Berne, Switzerland, 1994, 177\u2013194."},{"key":"15_CR9","first-page":"154","volume":"697","author":"H. Hungar","year":"1993","unstructured":"H. Hungar, \u201cCombining Model Checking and Theorem Proving to Verify Parallel Processes\u201d, 5th International Conference on Computer Aided Verification, Elounda, Greece, June\/July 1993, LNCS 697, pp.154\u2013165.","journal-title":"LNCS"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan, Computer-Aided Verification of Coordinating Processes, Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"15_CR11","first-page":"166","volume":"697","author":"R.P. Kurshan","year":"1993","unstructured":"R.P. Kurshan and L. Lamport, \u201cVerification of a Multiplier: 64 Bits and Beyond\u201d, 5th International Conference on Computer Aided Verification, Elounda, Greece, June\/July 1993, LNCS 697, pp.166\u2013179.","journal-title":"LNCS"},{"key":"15_CR12","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF01887206","volume":"1","author":"M. Z. Kwiatkowska","year":"1989","unstructured":"M. Z. Kwiatkowska, Event Fairness and Non-Interleaving Concurrency, Formal Aspects of Computing 1 (1989), 213\u2013228.","journal-title":"Formal Aspects of Computing"},{"key":"15_CR13","unstructured":"L. Lamport, What good is temporal logic, in R.E.A. Mason (ed.), Proceedings of IFIP Congress, North Holland, 1983, 657\u2013668."},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science 255","first-page":"279","volume-title":"Advances in Petri Nets 1986","author":"A. Mazurkiewicz","year":"1987","unstructured":"A. Mazurkiewicz, Trace Theory, in: W. Brauer, W. Reisig, G. Rozenberg (eds.) Advances in Petri Nets 1986, Bad Honnef, Germany, Lecture Notes in Computer Science 255, Springer, 1987, 279\u2013324."},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Thomas F. Melham, \u201cAutomating Recursive Type Definitions in Higher-Order Logic\u201d, pp. 341\u2013386 of G. Birtwistle and P.A. Subrahmanyam (Ed.), Current Trends in Hardware Verification and Automated Theorem Proving, Springer-Verlag, 1989.","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"15_CR16","first-page":"377","volume":"818","author":"D. Peled","year":"1994","unstructured":"D. Peled, Combining Partial Order Reductions with On-the-fly Model-Checking, 6th International Conference on Computer Aided Verification, Stanford, CA, USA, 1994, LNCS 818, 377\u2013390.","journal-title":"LNCS"},{"key":"15_CR17","first-page":"84","volume":"939","author":"S. Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, M.K. Srivas, An Integration of Model Checking with Automated Proof Checking, 7th International Conference on Computer Aided Verification, Li\u00e8ge, Belgium, July 1995, LNCS 939, 84\u201397.","journal-title":"LNCS"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Wolfgang Thomas, \u201cutomata on Infinite Objects\u201d, pp.133\u2013192 of Jan van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics, The MIT Press\/Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61042-1_48.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:03:34Z","timestamp":1605647014000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61042-1_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540610427","9783540498742"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-61042-1_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}