{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:22Z","timestamp":1775873662122,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642397981","type":"print"},{"value":"9783642397998","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_53","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T19:13:06Z","timestamp":1373483586000},"page":"756-772","source":"Crossref","is-referenced-by-count":37,"title":["Effectively-Propositional Reasoning about Reachability in Linked Data Structures"],"prefix":"10.1007","author":[{"given":"Shachar","family":"Itzhaky","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anindya","family":"Banerjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neil","family":"Immerman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aleksandar","family":"Nanevski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"53_CR1","unstructured":"SMTLIB: Satisfiability modulo theories library, \n                    \n                      http:\/\/smtlib.cs.uiowa.edu\/docs.html"},{"key":"53_CR2","unstructured":"Technical report, \n                    \n                      http:\/\/www.cs.tau.ac.il\/~shachar\/dl\/tr-2013.pdf"},{"key":"53_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-33386-6_14","volume-title":"Automated Technology for Verification and Analysis","author":"A. Bouajjani","year":"2012","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 167\u2013182. Springer, Heidelberg (2012)"},{"key":"53_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"53_CR5","doi-asserted-by":"crossref","unstructured":"Demetrescu, C., Italiano, G.F.: Decremental all-pairs shortest paths. In: Encyclopedia of Algorithms (2008)","DOI":"10.1007\/978-0-387-30162-4_102"},{"key":"53_CR6","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/344788.344808","volume":"29","author":"G. Dong","year":"2000","unstructured":"Dong, G., Su, J.: Incremental maintenance of recursive views using relational calculus\/sql. SIGMOD Record\u00a029, 44\u201351 (2000)","journal-title":"SIGMOD Record"},{"key":"53_CR7","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: POPL (2001)","DOI":"10.1145\/360204.360220"},{"issue":"3","key":"53_CR8","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1016\/j.cosrev.2011.02.002","volume":"5","author":"M. Frade","year":"2011","unstructured":"Frade, M., Pinto, J.: Verification conditions for source-level imperative programs. Computer Science Review\u00a05(3), 252\u2013277 (2011)","journal-title":"Computer Science Review"},{"key":"53_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Henriksen","year":"1995","unstructured":"Henriksen, J., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, pp. 89\u2013110. Springer, Heidelberg (1995)"},{"key":"53_CR10","unstructured":"Hesse, W.: Dynamic computational complexity. PhD thesis, Dept. of Computer Science, University of Massachusetts, Amherst, MA (2003)"},{"key":"53_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-30124-0_15","volume-title":"Computer Science Logic","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundary between decidability and undecidability for transitive-closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 160\u2013174. Springer, Heidelberg (2004)"},{"issue":"2","key":"53_CR12","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/226643.226644","volume":"43","author":"H. Kautz","year":"1996","unstructured":"Kautz, H., Selman, B.: Knowledge compilation and theory approximation. J. ACM\u00a043(2), 193\u2013224 (1996)","journal-title":"J. ACM"},{"key":"53_CR13","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using smt solvers. In: POPL (2008)","DOI":"10.1145\/1328438.1328461"},{"key":"53_CR14","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. Logical Methods in Computer Science\u00a05(2) (2009)","DOI":"10.2168\/LMCS-5(2:12)2009"},{"key":"53_CR15","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: POPL (2011)","DOI":"10.1145\/1926385.1926455"},{"key":"53_CR16","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress, pp. 21\u201328 (1962)"},{"key":"53_CR17","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: PLDI (2001)","DOI":"10.1145\/378795.378851"},{"key":"53_CR18","doi-asserted-by":"crossref","unstructured":"Nelson, G.: Verifying reachability invariants of linked structures. In: POPL (1983)","DOI":"10.1145\/567067.567073"},{"issue":"4","key":"53_CR19","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10817-009-9161-6","volume":"44","author":"R. Piskac","year":"2010","unstructured":"Piskac, R., de Moura, L.M., Bj\u00f8rner, N.: Deciding effectively propositional logic using dpll and substitution sets. J. Autom. Reasoning\u00a044(4), 401\u2013424 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"53_CR20","doi-asserted-by":"crossref","unstructured":"Reps, T.W., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. ACM Trans. Program. Lang. Syst.\u00a032(6) (2010)","DOI":"10.1145\/1749608.1749613"},{"key":"53_CR21","doi-asserted-by":"crossref","unstructured":"Rinetzky, N., Bauer, J., Reps, T.W., Sagiv, S., Wilhelm, R.: A semantics for procedure local heaps and its abstractions. In: POPL (2005)","DOI":"10.1145\/1040305.1040330"},{"issue":"1-2","key":"53_CR22","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.jlap.2006.12.001","volume":"73","author":"G. Yorsh","year":"2007","unstructured":"Yorsh, G., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. J. Log. Algebr. Program\u00a073(1-2), 111\u2013142 (2007)","journal-title":"J. Log. Algebr. Program"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_53","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T14:43:20Z","timestamp":1557931400000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}