{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T23:10:03Z","timestamp":1749683403010,"version":"3.41.0"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319487489"},{"type":"electronic","value":"9783319487496"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-48749-6_55","type":"book-chapter","created":{"date-parts":[[2016,10,30]],"date-time":"2016-10-30T08:16:59Z","timestamp":1477815419000},"page":"735-743","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Using Unified Model Checking to Verify Heaps"],"prefix":"10.1007","author":[{"given":"Xu","family":"Lu","sequence":"first","affiliation":[]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,31]]},"reference":[{"key":"55_CR1","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th Annual IEEE Symposium on Logic in Computer Science, Computer Society, pp. 55\u201374. IEEE, Washington (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"55_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"issue":"6","key":"55_CR3","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM (JACM) 58(6), 26 (2011)","journal-title":"J. ACM (JACM)"},{"key":"55_CR4","unstructured":"Lu, X., Duan, Z., Tian, C.: Extending PPTL for verifying heap evolution properties. arXiv preprint arXiv:1507.08426 (2015)"},{"key":"55_CR5","unstructured":"Duan, Z.: An extended interval temporal logic and a framing technique for temporal logic programming. Ph.D. thesis, University of Newcastle upon Tyne (1996)"},{"issue":"1","key":"55_CR6","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.scico.2007.09.001","volume":"70","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Program. 70(1), 31\u201361 (2008)","journal-title":"Sci. Comput. Program."},{"key":"55_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-88194-0_12","volume-title":"Formal Methods and Software Engineering","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Tian, C.: A unified model checking approach with projection temporal logic. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 167\u2013186. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-88194-0_12"},{"issue":"5","key":"55_CR8","doi-asserted-by":"publisher","first-page":"755","DOI":"10.1093\/jigpal\/jzl009","volume":"14","author":"E Yahav","year":"2006","unstructured":"Yahav, E., Reps, T.W., Sagiv, S., Wilhelm, R.: Verifying temporal heap properties specified via evolution logic. Logic J. IGPL 14(5), 755\u2013783 (2006)","journal-title":"Logic J. IGPL"},{"key":"55_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/11804192_14","volume-title":"Formal Methods for Components and Objects","author":"D Distefano","year":"2006","unstructured":"Distefano, D., Katoen, J.-P., Rensink, A.: Safety and liveness in concurrent pointer programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 280\u2013312. Springer, Heidelberg (2006). doi: 10.1007\/11804192_14"},{"key":"55_CR10","unstructured":"Rieger, S.: Verification of pointer programs. Ph.D. thesis, RWTH Aachen University (2009)"},{"issue":"2\u20134","key":"55_CR11","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10817-009-9124-y","volume":"42","author":"M del Mar Gallardo","year":"2009","unstructured":"del Mar Gallardo, M., Merino, P., San\u00e1n, D.: Model checking dynamic memory allocation in operating systems. J. Autom. Reasoning 42(2\u20134), 229\u2013264 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"55_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-319-11737-9_29","volume-title":"Formal Methods and Software Engineering","author":"N Zhang","year":"2014","unstructured":"Zhang, N., Duan, Z., Tian, C.: Extending MSVL with function calls. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 446\u2013458. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-11737-9_29"},{"key":"55_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1007\/978-3-319-08608-8","volume-title":"Structured Object-Oriented Formal Language and Method","author":"X Wang","year":"2014","unstructured":"Wang, X., Duan, Z., Zhao, L.: Formalizing and implementing types in MSVL. In: Liu, S., Duan, Z. (eds.) SOFL+MSVL 2013. LNCS, vol. 8332, pp. 60\u201373. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Combinatorial Optimization and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48749-6_55","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T22:35:21Z","timestamp":1749681321000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48749-6_55"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319487489","9783319487496"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48749-6_55","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"31 October 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"COCOA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Combinatorial Optimization and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hong Kong","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 December 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 December 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cocoa2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conference.cs.cityu.edu.hk\/cocoa2016\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}