{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:12:02Z","timestamp":1725484322975},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439417"},{"type":"electronic","value":"9783540456223"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45622-8_1","type":"book-chapter","created":{"date-parts":[[2007,5,23]],"date-time":"2007-05-23T14:45:20Z","timestamp":1179931520000},"page":"1-17","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking and Abstraction"],"prefix":"10.1007","author":[{"given":"Robert P.","family":"Kurshan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"1_CR1","first-page":"844","volume":"36","author":"J. Barwise","year":"1989","unstructured":"J. Barwise, Mathematical proofs of computer system correctness, Notices Amer. Math. Soc. 36 (1989), 844\u2013851.","journal-title":"Notices Amer. Math. Soc."},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"W. W. Bledsoe and D. W. Loveland (eds.), Automated Theorem Proving: After 25 Years, Contemporary Math., vol. 9, Amer. Math. Soc., Providence, 1984; especially R. S. Boyer and J. S. Moore, Proof-checking, theorem-proving and program verification, pp. 119\u2013132.","DOI":"10.1090\/conm\/029\/07"},{"key":"1_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Logic of Programs: Workshop, Yorktown Heights, NY, May 1981","author":"E. M. Clarke","year":"1981","unstructured":"E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, Lecture Notes in Computer Science, vol. 131, Springer-Verlag, 1981."},{"key":"1_CR4","unstructured":"E. M. Clarke Jr., O. Grumberg, and D. Peled, Model Checking, MIT Press, 1999."},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"R. DeMillo, R. Lipton, and A. Perlis, Social processes and proofs of theorems and programs, Comm. ACM22 (1979), 271\u2013280.","DOI":"10.1145\/359104.359106"},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF00289519","volume":"1","author":"E. W. Dijkstra","year":"1971","unstructured":"E. W. Dijkstra, Hierarchical ordering of sequential processes, Acta Informatica 1 (1971), 115\u2013138.","journal-title":"Acta Informatica"},{"key":"1_CR7","first-page":"995","volume":"B","author":"E. A. Emerson","year":"1990","unstructured":"E. A. Emerson, Temporal and modal logic, Handbook of Theoretical Computer Science, vol. B, Elsevier, 1990, pp. 995\u20131072.","journal-title":"Handbook of Theoretical Computer Science"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"P. Halmos, Lectures on Boolean Algebras, Springer-Verlag, 1974.","DOI":"10.1007\/978-1-4612-9855-7"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan, Computer-aided Verification of Coordinating Processes\u2014The Automata-Theoretic Approach, Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"K. L. McMillan, Symbolic Model Checking, Kluwer, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"1_CR11","unstructured":"S. Schroeder, Turning to formal verification, Integrated System Design Magazine, Sept. 1997, 1\u20135."},{"key":"1_CR12","unstructured":"M. Y. Vardi and P. Wolper, An automata-theoretic approach to automatic program verification, Proc. (1st) IEEE Symposium on Logic in Computer Science, (1981), 322\u2013331."},{"key":"1_CR13","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/362575.362577","volume":"14","author":"N. Wirth","year":"1971","unstructured":"N. Wirth, Program development by stepwise refinement, Comm. ACM 14 (1971), pp. 221\u2013227.","journal-title":"Comm. ACM"}],"container-title":["Lecture Notes in Computer Science","Abstraction, Reformulation, and Approximation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45622-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T03:31:25Z","timestamp":1556422285000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45622-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439417","9783540456223"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-45622-8_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}