{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T09:00:39Z","timestamp":1766048439976},"publisher-location":"Boston, MA","reference-count":20,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9781475752755"},{"type":"electronic","value":"9780387356082"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/978-0-387-35608-2_36","type":"book-chapter","created":{"date-parts":[[2013,12,29]],"date-time":"2013-12-29T21:57:25Z","timestamp":1388354245000},"page":"435-447","source":"Crossref","is-referenced-by-count":8,"title":["Model Checking Birth and Death"],"prefix":"10.1007","author":[{"given":"Dino","family":"Distefano","sequence":"first","affiliation":[]},{"given":"Arend","family":"Rensink","sequence":"additional","affiliation":[]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"36_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M Abadi","year":"1999","unstructured":"M. Abadi, A. Gordon. A calculus for cryptographic protocols: The spi calculus. Inf. and Comp. 148 (1): 1\u201370, 1999.","journal-title":"Inf. and Comp."},{"issue":"3","key":"36_CR2","doi-asserted-by":"crossref","first-page":"207226","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"M. Ben-Ari, A. Pnueli, Z. Manna. The temporal logic of branching time. Acta Inf. 20(3):207226,1983.","journal-title":"Acta Inf"},{"key":"36_CR3","volume-title":"TACS01, LNCS 2255:1-37, Springer","author":"L Caires","year":"2001","unstructured":"L. Caires, L. Cardelli. A spatial logic for concurrency (part I). In TACS\u201901, LNCS 2255:1\u201337, Springer, 2001."},{"key":"36_CR4","volume-title":"TLCA01, LNCS 2044:46-60, Springer","author":"L Cardelli","year":"2001","unstructured":"L. Cardelli, A. Gordon. Logical properties of name restriction. In TLCA\u201901, LNCS 2044:46\u201360, Springer, 2001."},{"key":"36_CR5","volume-title":"FoSSaCS98, LNCS 1378:140-155, Springer","author":"L Cardelli","year":"1998","unstructured":"L. Cardelli, A. Gordon. Mobile ambients. In FoSSaCS\u201998, LNCS 1378:140\u2013155, Springer, 1998."},{"key":"36_CR6","volume-title":"Workshop on Logics of Programs, LNCS 131:52-71, Springer","author":"E Clarke","year":"1981","unstructured":"E. Clarke, E. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on Logics of Programs, LNCS 131:52\u201371, Springer, 1981."},{"key":"36_CR7","volume-title":"ICSE00 pp. 439-448, IEEE CS Press","author":"M Corbett","year":"2000","unstructured":"Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, H. Zheng. Bandera: Extracting finite-state models from Java source code. In ICSE\u201900 pp. 439\u2013448, IEEE CS Press, 2000."},{"key":"36_CR8","volume-title":"FMOODS00, pp. 305-326, Kluwer","author":"D Distefano","year":"2000","unstructured":"D. Distefano, J.-P. Katoen, A. Rensink. On a temporal logic for object-based systems. In FMOODS\u201900, pp. 305\u2013326, Kluwer, 2000."},{"key":"36_CR9","unstructured":"D. Distefano, A. Rensink J.-P. Katoen. Model checking dynamic allocation and deallocation. Technical report TR-01\u201340, University of Twente, 2002. Available on line at http:\/\/fmt.cs.utwente.nh\/`ddino\/papers\/DSRK01-report.ps.gz"},{"key":"36_CR10","volume-title":"Logic of Programs, LNCS 193:79-88, Springer","author":"EA Emerson","year":"1985","unstructured":"E. A. Emerson. Automata, tableaux and temporal logics. In Logic of Programs, LNCS 193:79\u201388, Springer, 1985."},{"key":"36_CR11","first-page":"235","volume-title":"Theory and Formal Methods","author":"J Fiadeiro","year":"1995","unstructured":"J. Fiadeiro, T. Maibaum. Verifying for reuse: foundations of object-oriented system verification. In Theory and Formal Methods, pp. 235\u2013257, 1995."},{"issue":"4","key":"36_CR12","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"K. Havelund, T. Pressburger. Model checking Java programs using Java PathFinder. Int. J. on Software Tools for Technology Transfer, 2 (4): 366\u2013381, 2000.","journal-title":"Int. J. on Software Tools for Technology Transfer"},{"key":"36_CR13","doi-asserted-by":"crossref","unstructured":"Kupferman, M. Y. Vardi, P. Wolper. An automata-theoretic approach to branching-time model checking. J. of the ACM, 47 (2): 312\u2013360, 2000.","DOI":"10.1145\/333979.333987"},{"key":"36_CR14","doi-asserted-by":"crossref","unstructured":"Lichtenstein, A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In POPL\u201985, pp. 97\u2013107, ACM Press, 1985.","DOI":"10.1145\/318593.318622"},{"issue":"1","key":"36_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"R. Milner, J. Parrow, D. Walker. A calculus of mobile processes. Inf. and Comp. 100 (1): 1\u201377, 1992.","journal-title":"Inf. and Comp."},{"key":"36_CR16","doi-asserted-by":"crossref","unstructured":"U. Montanari, M. Pistore. An introduction to history-dependent automata. Electr. Notes in Th. Comp. Sci., 10, 1998.","DOI":"10.1016\/S1571-0661(05)80696-6"},{"key":"36_CR17","volume-title":"FOCS77, pp. 46-57, IEEE CS Press","author":"A Pnueli","year":"1977","unstructured":"A. Pnueli. The temporal logic of programs. In FOCS\u201977, pp. 46\u201357, IEEE CS Press, 1977."},{"issue":"5","key":"36_CR18","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1093\/logcom\/5.5.603","volume":"5","author":"A Sernadas","year":"1995","unstructured":"A. Sernadas, C. Sernadas, J.F. Costa. Object specification logic. J. of Logic and Computation, 5 (5): 603\u2013630, 1995.","journal-title":"J. of Logic and Computation"},{"key":"36_CR19","volume-title":"L1CS86, pp. 332-344, IEEE CS Press","author":"MY Vardi","year":"1986","unstructured":"M. Y. Vardi, R Wolper. An automata-theoretic approach to automatic program verification. In L1CS\u201986, pp. 332\u2013344, IEEE CS Press, 1986."},{"key":"36_CR20","volume-title":"POPL 2001 pp. 27-40 ACM Press","author":"E Yahay","year":"2001","unstructured":"E. Yahay. Verifying safety properties of concurrent Java programs using 3-valued logic. In POPL\n                    2001, pp. 27\u201340 ACM Press, 2001."}],"container-title":["Foundations of Information Technology in the Era of Network and Mobile Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-0-387-35608-2_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T00:59:21Z","timestamp":1557795561000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-0-387-35608-2_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9781475752755","9780387356082"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-0-387-35608-2_36","relation":{},"subject":[],"published":{"date-parts":[[2002]]}}}