{"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":1775873662137,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,1,8]],"date-time":"2014-01-08T00:00:00Z","timestamp":1389139200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,1,8]]},"DOI":"10.1145\/2535838.2535854","type":"proceedings-article","created":{"date-parts":[[2014,1,14]],"date-time":"2014-01-14T08:40:06Z","timestamp":1389688806000},"page":"385-396","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Modular reasoning about heap paths via effectively propositional formulas"],"prefix":"10.1145","author":[{"given":"Shachar","family":"Itzhaky","sequence":"first","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anindya","family":"Banerjee","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neil","family":"Immerman","sequence":"additional","affiliation":[{"name":"UMASS Amherst, Amherst, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aleksandar","family":"Nanevski","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,1,8]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Context-bounded analysis for concurrent programs with dynamic creation of threads. Logical Methods in Computer Science, 7(4)","author":"Atig M. F.","year":"2011","unstructured":"M. F. Atig , A. Bouajjani , and S. Qadeer . Context-bounded analysis for concurrent programs with dynamic creation of threads. Logical Methods in Computer Science, 7(4) , 2011 . M. F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. Logical Methods in Computer Science, 7(4), 2011."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_3_2_2_3_1","volume-title":"SMTLIB: Satisfiability Modulo Theories Library","author":"Barrett C.","year":"2013","unstructured":"C. Barrett , A. Stump , , and C. Tinelli . SMTLIB: Satisfiability Modulo Theories Library , 2013 . http:\/\/smtlib.cs.uiowa.edu\/docs.html. C. Barrett, A. Stump, , and C. Tinelli. SMTLIB: Satisfiability Modulo Theories Library, 2013. http:\/\/smtlib.cs.uiowa.edu\/docs.html."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_14"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1102"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_16"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0539-5","volume-title":"Descriptive complexity. Graduate texts in computer science","author":"Immerman N.","year":"1999","unstructured":"N. Immerman . Descriptive complexity. Graduate texts in computer science . Springer , 1999 . N. Immerman. Descriptive complexity. Graduate texts in computer science. Springer, 1999."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_3_2_2_10_1","volume-title":"Modular reasoning about heap paths via effectively propositional formulas. Technical report","author":"Itzhaky S.","year":"2013","unstructured":"S. Itzhaky , A. Banerjee , N. Immerman , O. Lahav , A. Nanevski , and M. Sagiv . Modular reasoning about heap paths via effectively propositional formulas. Technical report , Tel Aviv University , 2013 . http:\/\/www.cs.tau.ac.il\/~shachar\/dl\/tr 2013b.pdf. S. Itzhaky, A. Banerjee, N. Immerman, O. Lahav, A. Nanevski, and M. Sagiv. Modular reasoning about heap paths via effectively propositional formulas. Technical report, Tel Aviv University, 2013. http:\/\/www.cs.tau.ac.il\/~shachar\/dl\/tr 2013b.pdf."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958053"},{"key":"e_1_3_2_2_12_1","volume-title":"Effectively-propositional reasoning about reachability in linked data structures. Technical report","author":"Itzhaky S.","year":"2013","unstructured":"S. Itzhaky , A. Banerjee , N. Immerman , A. Nanevski , and M. Sagiv . Effectively-propositional reasoning about reachability in linked data structures. Technical report , Tel Aviv University , 2013 . http:\/\/www.cs.tau.ac.il\/~shachar\/dl\/tr-2013.pdf. S. Itzhaky, A. Banerjee, N. Immerman, A. Nanevski, and M. Sagiv. Effectively-propositional reasoning about reachability in linked data structures. Technical report, Tel Aviv University, 2013. http:\/\/www.cs.tau.ac.il\/~shachar\/dl\/tr-2013.pdf."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328461"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926455"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_5"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9161-6"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958054"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040330"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_20"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926406"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/321879.321884"},{"key":"e_1_3_2_2_25_1","volume-title":"The CMU Larch Project","author":"Wing J.","year":"1995","unstructured":"J. Wing . The CMU Larch Project . 1995 . URL http:\/\/www.cs.cmu.edu\/afs\/cs\/project\/larch\/www\/home.html. J. Wing. The CMU Larch Project. 1995. URL http:\/\/www.cs.cmu.edu\/afs\/cs\/project\/larch\/www\/home.html."},{"key":"e_1_3_2_2_26_1","series-title":"Foundations of Computing Series","volume-title":"An Introduction","author":"Winskel G.","year":"1993","unstructured":"G. Winskel . The Formal Semantics of Programming Languages : An Introduction . Foundations of Computing Series . Zone Books , U.S. , 1993 . ISBN 9780262731034. G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing Series. Zone Books, U.S., 1993. ISBN 9780262731034."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_36"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2006.12.001"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375624"}],"event":{"name":"POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"San Diego California USA","acronym":"POPL '14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535854","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2535838.2535854","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:06Z","timestamp":1750219806000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535854"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1,8]]},"references-count":28,"alternative-id":["10.1145\/2535838.2535854","10.1145\/2535838"],"URL":"https:\/\/doi.org\/10.1145\/2535838.2535854","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2578855.2535854","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,1,8]]},"assertion":[{"value":"2014-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}