{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:32:19Z","timestamp":1778297539674,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540430025","type":"print"},{"value":"9783540452942","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45294-x_25","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T22:45:12Z","timestamp":1181601912000},"page":"292-304","source":"Crossref","is-referenced-by-count":35,"title":["From Falsification to Verification"],"prefix":"10.1007","author":[{"given":"Doron","family":"Peled","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lenore","family":"Zuck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,11,26]]},"reference":[{"key":"25_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Design and synthesis of synchronization skeletons usingbranc hingtime temporal logic","author":"E.M. Clarke","year":"1982","unstructured":"E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons usingbranc hingtime temporal logic. In Proc. IBM Workshop on Logics of Programs, LNCS 131, 1981."},{"key":"25_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"ICALP\u201980","author":"E.A. Emerson","year":"1980","unstructured":"E.A. Emerson and E.M. Clarke. Characterizingcorrectness properties of parallel programs using fixpoints. In ICALP\u201980, pp. 169\u2013181, LNCS 85."},{"key":"25_CR3","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Y. Kesten and A. Pnueli. Verification by finitary abstraction. Information and Computation, 163:203\u2013243, 2000.","journal-title":"Information and Computation"},{"key":"25_CR4","doi-asserted-by":"crossref","DOI":"10.1515\/9781400864041","volume-title":"Computer Aided Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1995","unstructured":"R.P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton University Press, Princeton, New Jersey, 1995."},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checkingthat finite-state concurrent programs satisfy their linear specification. In POPL\u201985, pp. 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"25_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"LICS\u201985","author":"O. Lichtenstein","year":"1985","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In LICS\u201985, LNCS 193, pp. 196\u2013218, 1985."},{"key":"25_CR7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991."},{"key":"25_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995."},{"key":"25_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-44585-4_2","volume-title":"CAV\u201901","author":"K.S. Namjoshi","year":"2001","unstructured":"K.S. Namjoshi. Certifyingmo del checkers. In CAV\u201901, LNCS 2102, pp. 2\u201313."},{"key":"25_CR10","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"SPIN\u20192001","author":"D. Peled","year":"2001","unstructured":"D. Peled and L. Zuck. From model checkingto a temporal proof. In SPIN\u20192001, LNCS 2057pp. 1\u201314."},{"key":"25_CR11","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS\u201986, pp. 332\u2013344, 1986."}],"container-title":["Lecture Notes in Computer Science","FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45294-X_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T21:28:00Z","timestamp":1556486880000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45294-X_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540430025","9783540452942"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-45294-x_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}