{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:37:00Z","timestamp":1742913420605,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319049144"},{"type":"electronic","value":"9783319049151"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-04915-1_3","type":"book-chapter","created":{"date-parts":[[2014,2,20]],"date-time":"2014-02-20T15:12:22Z","timestamp":1392909142000},"page":"35-47","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Integrating Separation Logic with PPTL"],"prefix":"10.1007","author":[{"given":"Xu","family":"Lu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongjin","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,2,21]]},"reference":[{"key":"3_CR1","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. J. Mach. Intell. 7, 23\u201350 (1972)","journal-title":"J. Mach. Intell."},{"key":"3_CR2","series-title":"LNCS","first-page":"1","volume-title":"ECCOP 1999","author":"CAR Hoare","year":"1999","unstructured":"Hoare, C.A.R., He, J.: A trace model for pointers and objects. In: Guerraoui, R. (ed.) ECCOP 1999. LNCS, vol. 1628, pp. 1\u201317. Springer, Heidelberg (1999)"},{"key":"3_CR3","first-page":"296","volume-title":"In: PLDI","author":"DR Chase","year":"1990","unstructured":"Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of pointers and structures. In: PLDI, pp. 296\u2013310. ACM Press, New York (1990)"},{"key":"3_CR4","series-title":"LNCS","first-page":"1","volume-title":"CC\/ETAPS 2000","author":"R Wilhelm","year":"2000","unstructured":"Wilhelm, R., Sagiv, S., Reps, T.W.: Shape analysis. In: Watt, D.A. (ed.) CC\/ETAPS 2000. LNCS, vol. 1781, pp. 1\u201317. Springer, Heidelberg (2000)"},{"key":"3_CR5","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. J. ACM Trans. Program. Lang. Syst. 24, 217\u2013298 (2002)","journal-title":"J. ACM Trans. Program. Lang. Syst."},{"key":"3_CR6","series-title":"LNCS","first-page":"280","volume-title":"SAS 2000","author":"T Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280\u2013302. Springer, Heidelberg (2000)"},{"key":"3_CR7","first-page":"55","volume-title":"In: 17th IEEE Symp. on Logic in Comput. Sci.","author":"JC Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th IEEE Symp. on Logic in Comput. Sci., pp. 55\u201374. IEEE Press, New York (2002)"},{"key":"3_CR8","series-title":"LNCS","first-page":"52","volume-title":"ALAPS 2005","author":"J Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) ALAPS 2005. LNCS, vol. 3780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"key":"3_CR9","series-title":"LNCS","first-page":"287","volume-title":"TACAS 2006","author":"D Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"3_CR10","series-title":"LNCS","first-page":"395","volume-title":"FoSSaCS 2005","author":"C Calcagno","year":"2005","unstructured":"Calcagno, C., Gardner, P., Hague, M.: From separation logic to first-order logic. In: Sassone, V. (ed.) FoSSaCS 2005. LNCS, vol. 3441, pp. 395\u2013409. Springer, Heidelberg (2005)"},{"key":"3_CR11","unstructured":"Moszkowski, B.C.: Reasoning about digital circuits. Ph.D. thesis, Stanford University (1983)"},{"key":"3_CR12","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)"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/BF02944904","volume":"19","author":"Z Duan","year":"2004","unstructured":"Duan, Z., Koutny, M.: A framed temporal logic programming language. J. Comput. Sci. Technol. 19, 341\u2013351 (2004)","journal-title":"J. Comput. Sci. Technol."},{"key":"3_CR14","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. J. Sci. Comput. Program. 70, 31\u201361 (2008)","journal-title":"J. Sci. Comput. Program."},{"key":"3_CR15","series-title":"LNCS","first-page":"204","volume-title":"ESOP 2003","author":"E Yahav","year":"2003","unstructured":"Yahav, E., Reps, T., Sagiv, M., Wilhelm, R.: Verifying temporal heap properties specified via evolution logic. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 204\u2013222. Springer, Heidelberg (2003)"},{"key":"3_CR16","series-title":"LNCS","first-page":"280","volume-title":"FMCO 2005","author":"D Distefano","year":"2006","unstructured":"Distefano, D., Katoen, J.-P., Rensink, A.: Safety and liveness in concurrent pointer programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 280\u2013312. Springer, Heidelberg (2006)"},{"key":"3_CR17","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. Reason. 42, 229\u2013264 (2009)","journal-title":"J. Autom. Reason."},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/j.apal.2009.07.004","volume":"161","author":"R Brochenin","year":"2009","unstructured":"Brochenin, R., Demri, S., Lozes, E.: Reasoning about sequences of memory states. J. Ann. Pure Appl. Logic 161, 305\u2013323 (2009)","journal-title":"J. Ann. Pure Appl. Logic"},{"key":"3_CR19","series-title":"LNCS","first-page":"108","volume-title":"FSTTCS 2001","author":"C Calcagno","year":"2001","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108\u2013119. Springer, Heidelberg (2001)"},{"key":"3_CR20","series-title":"LNCS","first-page":"97","volume-title":"FSTTCS 2004","author":"J Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 97\u2013109. Springer, Heidelberg (2004)"},{"key":"3_CR21","series-title":"LNCS","first-page":"167","volume-title":"ICFEM 2008","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)"},{"key":"3_CR22","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","volume":"45","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. J. Acta Inform. 45, 43\u201378 (2008)","journal-title":"J. Acta Inform."},{"key":"3_CR23","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1017\/S096012950800738X","volume":"19","author":"C Tian","year":"2009","unstructured":"Tian, C., Duan, Z.: Complexity of propositional projection temporal logic with star. J. Math. Struct. Comput. Sci. 19, 73\u2013100 (2009)","journal-title":"J. Math. Struct. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-04915-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,7]],"date-time":"2023-02-07T22:12:24Z","timestamp":1675807944000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-04915-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319049144","9783319049151"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-04915-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"21 February 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}