{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:12:55Z","timestamp":1763467975440},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,7,6]],"date-time":"2010-07-06T00:00:00Z","timestamp":1278374400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2010,8]]},"DOI":"10.1007\/s10817-010-9179-9","type":"journal-article","created":{"date-parts":[[2010,7,5]],"date-time":"2010-07-05T07:20:41Z","timestamp":1278314441000},"page":"131-156","source":"Crossref","is-referenced-by-count":13,"title":["Quantitative Separation Logic and Programs with Lists"],"prefix":"10.1007","volume":"45","author":[{"given":"Marius","family":"Bozga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Swann","family":"Perarnau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,7,6]]},"reference":[{"key":"9179_CR1","unstructured":"ARMC. http:\/\/www.mpi-sb.mpg.de\/~rybal\/armc\/ . Accessed 30 June 2010"},{"key":"9179_CR2","unstructured":"ASPIC. http:\/\/laure.gonnord.org\/pro\/aspic\/aspic.html . Accessed 30 June 2010"},{"key":"9179_CR3","unstructured":"L2CA. http:\/\/www-verimag.imag.fr\/~async\/L2CA\/l2ca.html . Accessed 30 June 2010"},{"key":"9179_CR4","unstructured":"Smallfoot. http:\/\/www.dcs.qmul.ac.uk\/research\/logic\/theory\/projects\/smallfoot\/index.html . Accessed 30 June 2010"},{"key":"9179_CR5","series-title":"LNCS","first-page":"368","volume-title":"Proc. CAV","author":"A Annichini","year":"2001","unstructured":"Annichini, A., Bouajjani, A., Sighireanu, M.: Trex: a tool for reachability analysis of complex systems. In: Proc. CAV. LNCS, vol. 2102, pp. 368\u2013372. Springer, Heidelberg (2001)"},{"key":"9179_CR6","series-title":"LNCS","volume-title":"Proc. TACAS","author":"S Bardin","year":"2004","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: fast accelereation of symbolic transition systems. In: Proc. TACAS. LNCS, vol. 2725. Springer, Heidelberg (2004)"},{"key":"9179_CR7","volume-title":"Proc. European Symposium on Programming. LNCS","author":"M Benedikt","year":"1999","unstructured":"Benedikt, M., Reps, T., Sagiv, M.: A decidable logic for describing linked data structures. In: Proc. European Symposium on Programming. LNCS. Springer, Heidelberg (1999)"},{"key":"9179_CR8","series-title":"LNCS","volume-title":"FSTTCS","author":"J Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.: A decidable fragment of separation logic. In: FSTTCS. LNCS, vol. 3328. Springer, Heidelberg (2004)"},{"key":"9179_CR9","volume-title":"Proc. Computer Aided Verification (CAV). LNCS","author":"A Bouajjani","year":"2006","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: Proc. Computer Aided Verification (CAV). LNCS. Springer, Heidelberg (2006)"},{"key":"9179_CR10","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/978-3-642-04081-8_13","volume-title":"CONCUR 2009: Proceedings of the 20th International Conference on Concurrency Theory","author":"A Bouajjani","year":"2009","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: A logic-based framework for reasoning about composite data structures. In: CONCUR 2009: Proceedings of the 20th International Conference on Concurrency Theory, pp. 178\u2013195. Springer, Heidelberg (2009)"},{"key":"9179_CR11","first-page":"323","volume-title":"CSL \u201908: Proceedings of the 22nd International Workshop on Computer Science Logic","author":"R Brochenin","year":"2008","unstructured":"Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. In: CSL \u201908: Proceedings of the 22nd International Workshop on Computer Science Logic, pp. 323\u2013338. Springer, Heidelberg (2008)"},{"key":"9179_CR12","first-page":"23","volume":"7","author":"RM Burstall","year":"1972","unstructured":"Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Mach. Intell. 7, 23\u201350 (1972)","journal-title":"Mach. Intell."},{"key":"9179_CR13","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/978-3-540-73368-3_42","volume-title":"Computer Aided Verification","author":"S Gulwani","year":"2007","unstructured":"Gulwani, S., Tiwari, A.: An abstract domain for analyzing heap-manipulating low-level software. In: Computer Aided Verification. LNCS, vol. 4590, pp. 379\u2013392. Springer, Heidelberg (2007)"},{"key":"9179_CR14","series-title":"LNCS","volume-title":"CAV","author":"N Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: Verification via structure simulation. In: CAV. LNCS, vol. 3114. Springer, Heidelberg (2004)"},{"key":"9179_CR15","volume-title":"POPL","author":"S Ishtiaq","year":"2001","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: BI as an assertion language for mutable data structures. In: POPL. Springer, Heidelberg (2001)"},{"key":"9179_CR16","series-title":"LNCS","volume-title":"SAS","author":"S Magill","year":"2007","unstructured":"Magill, S., Berdine, J., Clarke, E., Cook, B.: Arithmetic strengthening for shape analysis. In: SAS. LNCS, vol. 4634. Springer, Heidelberg (2007)"},{"key":"9179_CR17","volume-title":"Computation: Finite and Infinite Machines","author":"M Minsky","year":"1967","unstructured":"Minsky, M.: Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs (1967)"},{"key":"9179_CR18","series-title":"LNCS","volume-title":"FSTTCS","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Calcagno, C., Yang, H.: Computability and complexity results for a spatial assertion language for data structures. In: FSTTCS. LNCS, vol. 2245. Springer, Heidelberg (2001)"},{"key":"9179_CR19","unstructured":"Presburger, M.: \u00dcber die Vollstandigkeit eines gewissen Systems der Arithmetik. In: Comptes Rendus du I Congr\u00e9s des Pays Slaves. Warsaw (1929)"},{"key":"9179_CR20","volume-title":"Proc. 17th IEEE Symposium on Logic in Computer Science. LNCS","author":"JC Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proc. 17th IEEE Symposium on Logic in Computer Science. LNCS. Springer, Heidelberg (2002)"},{"key":"9179_CR21","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/978-3-642-02959-2_5","volume-title":"CADE-22: Proceedings of the 22nd International Conference on Automated Deduction","author":"V Sofronie-Stokkermans","year":"2009","unstructured":"Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: CADE-22: Proceedings of the 22nd International Conference on Automated Deduction, pp. 67\u201383. Springer, Heidelberg (2009)"},{"key":"9179_CR22","first-page":"88","volume-title":"Proc. CAV. LNCS, vol. 1427","author":"P Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Proc. CAV. LNCS, vol. 1427, pp. 88\u201397. Springer, Heidelberg (1998)"},{"key":"9179_CR23","volume-title":"Proc. Foundations of Software Science and Computation Structures. LNCS","author":"G Yorsh","year":"2006","unstructured":"Yorsh, G., Rabinovich, A., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. In: Proc. Foundations of Software Science and Computation Structures. LNCS. Springer, Heidelberg (2006)"},{"issue":"10","key":"9179_CR24","doi-asserted-by":"crossref","first-page":"1526","DOI":"10.1016\/j.ic.2006.03.004","volume":"204","author":"T Zhang","year":"2006","unstructured":"Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for term algebras with integer constraints. Inf. Comput. 204(10), 1526\u20131574 (2006)","journal-title":"Inf. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9179-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9179-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9179-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:50Z","timestamp":1559265710000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9179-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7,6]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,8]]}},"alternative-id":["9179"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9179-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,7,6]]}}}