{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:39:48Z","timestamp":1725493188150},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008866"},{"type":"electronic","value":"9783540365754"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36575-3_15","type":"book-chapter","created":{"date-parts":[[2007,10,27]],"date-time":"2007-10-27T21:52:15Z","timestamp":1193521935000},"page":"204-222","source":"Crossref","is-referenced-by-count":24,"title":["Verifying Temporal Heap Properties Specified via Evolution Logic"],"prefix":"10.1007","author":[{"given":"Eran","family":"Yahav","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reinhard","family":"Wilhelm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"15_CR1","unstructured":"E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"J. C. Corbett, M. B. Dwyer, J. Hatcliff, and Robby. A language framework for expressing checkable properties of dynamic software. In SPIN, 2000.","DOI":"10.1007\/10722468_13"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"B. Courcelle. On the expression of graph properties in some fragments of monadic secondorder logic. In N. Immerman and P.G. Kolaitis, editors, Descriptive Complexity and Finite Models: Proceedings of a DIAMCSWorkshop, chapter 2, pages 33\u201357. American Mathematical Society, 1996.","DOI":"10.1090\/dimacs\/031\/02"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In POPL, 1977.","DOI":"10.1145\/512950.512973"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Temporal abstract interpretation. In Proc. of 27th POPL, pages 12\u201325, January 2000.","DOI":"10.1145\/325694.325699"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"N. Dor, M. Rodeh, and M. Sagiv. Checking cleanness in linked lists. In SAS. Springer, 2000.","DOI":"10.1007\/978-3-540-45099-3_7"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finitestate verification. In Proc. of Int. Conf. on Software Engineering, pages 411\u2013421, May 1999.","DOI":"10.1145\/302405.302672"},{"key":"15_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-011-5292-1","volume-title":"First-Order Modal Logic","author":"M. Fitting","year":"1998","unstructured":"M. Fitting and R.L. Mendelsohn. First-Order Modal Logic, volume 277 of Synthese Library. Kluwer Academic Publishers, Dordrecht, 1998."},{"key":"15_CR9","unstructured":"G.E. Hughes and M.J. Creswel. An Introduction to Modal Logic. Methuen, London, 1982."},{"key":"15_CR10","unstructured":"Y. Kesten, A. Pnueli, and M. Vardi. Verification by augmented abstraction: The automatatheoretic view. JCSS: J. of Comp. Sys. Sci., 62, 2001."},{"key":"15_CR11","unstructured":"T. Lev-Ami and M. Sagiv. TVLA: A framework for Kleene based static analysis. In Static Analysis Symposium. Springer, 2000."},{"key":"15_CR12","doi-asserted-by":"publisher","first-page":"113","DOI":"10.2307\/2024555","volume":"5","author":"D. Lewis","year":"1968","unstructured":"D. Lewis. Counterpart theory and quantified modal logic. Journal of Philosophy, LXV(5):113\u2013126, 1968.","journal-title":"Journal of Philosophy"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"A. Pnueli, J. Xu, and L. Zuck. Liveness with (0,1,infinity)-counter abstraction. CAV 2002.","DOI":"10.1007\/3-540-45657-0_9"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems, 24(3):217.","DOI":"10.1145\/514188.514190"},{"issue":"1","key":"15_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"M.Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, 15 November 1994.","journal-title":"Information and Computation"},{"key":"15_CR17","unstructured":"E. Yahav. http:\/\/www.cs.tau.ac.il\/.yahave ."},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"E. Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proc. of 27th POPL, pages 27\u201340, March 2001.","DOI":"10.1145\/360204.360206"},{"key":"15_CR19","series-title":"Technical Report","volume-title":"LTL model checking for systems with unbounded number of dynamically created threads and objects","author":"E. Yahav","year":"2001","unstructured":"E. Yahav, T. Reps, and M. Sagiv. LTL model checking for systems with unbounded number of dynamically created threads and objects. Technical Report TR-1424, CS Dept., Univ. of Wisconsin, Madison, WI, March 2001."},{"key":"15_CR20","series-title":"Technical Report","volume-title":"Automatic verification of temporal properties of concurrent heap-manipulating programs using evolution logic","author":"E. Yahav","year":"2002","unstructured":"E. Yahav, T. Reps, M. Sagiv, and R. Wilhelm. Automatic verification of temporal properties of concurrent heap-manipulating programs using evolution logic. Technical Report 338\/02, School of CS, Tel Aviv University, Israel, July 2002."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36575-3_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,27]],"date-time":"2020-04-27T17:21:37Z","timestamp":1588008097000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36575-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008866","9783540365754"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-36575-3_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}