{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T03:08:23Z","timestamp":1725937703171},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214363"},{"type":"electronic","value":"9783642214370"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21437-0_29","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T07:33:16Z","timestamp":1308382396000},"page":"386-401","source":"Crossref","is-referenced-by-count":7,"title":["Structured Specifications for Better Verification of Heap-Manipulating Programs"],"prefix":"10.1007","author":[{"given":"Cristian","family":"Gherghina","sequence":"first","affiliation":[]},{"given":"Cristina","family":"David","sequence":"additional","affiliation":[]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"29_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 115\u2013137. Springer, Heidelberg (2006)"},{"key":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BFb0031816","volume-title":"Formal Methods in Computer-Aided Design","author":"B. Brock","year":"1996","unstructured":"Brock, B., Kaufmann, M., Strother Moore, J.: ACL2 Theorems About Commercial Microprocessors. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 275\u2013293. Springer, Heidelberg (1996)"},{"key":"29_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers\u00a035, 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Software Tools for Technology Transfer (2005)","DOI":"10.1007\/s10009-004-0167-4"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Rival, X.: Relational inductive shape analysis. In: POPL, pp. 247\u2013260 (2008)","DOI":"10.1145\/1328438.1328469"},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Multiple pre\/post specifications for heap-manipulating methods. In: HASE, pp. 357\u2013364 (2007)","DOI":"10.1109\/HASE.2007.19"},{"key":"29_CR8","doi-asserted-by":"crossref","unstructured":"Distefano, D., Parkinson, M.J.: jStar: Towards Practical Verification for Java. In: OOPSLA (2008)","DOI":"10.1145\/1449764.1449782"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: ACM POPL, London, pp. 14\u201326 (January 2001)","DOI":"10.1145\/373243.375719"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-17164-2_21","volume-title":"Programming Languages and Systems","author":"B. Jacobs","year":"2010","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the veriFast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol.\u00a06461, pp. 304\u2013311. Springer, Heidelberg (2010)"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-44585-4_40","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2001","unstructured":"Jhala, R., McMillan, K.L.: Microarchitecture verification by compositional model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 396\u2013410. Springer, Heidelberg (2001)"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-54834-3_26","volume-title":"VDM \u201991","author":"H.B.M. Jonkers","year":"1991","unstructured":"Jonkers, H.B.M.: Upgrading the pre- and postcondition technique. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol.\u00a0551, pp. 428\u2013456. Springer, Heidelberg (1991)"},{"key":"29_CR13","unstructured":"Klarlund, N., Moller, A.: MONA Version 1.4 - User Manual. BRICS Notes Series (January 2001)"},{"key":"29_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1087","DOI":"10.1007\/3-540-48118-4_8","volume-title":"FM\u201999 - Formal Methods","author":"G.T. Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L.: Enhancing the pre- and postcondition technique for more expressive specifications. In: Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01709, p. 1087. Springer, Heidelberg (1999)"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Rustan","year":"2010","unstructured":"Rustan, K., Leino, M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: ACM POPL, pp. 247\u2013258 (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"29_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-69738-1_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H.H. Nguyen","year":"2007","unstructured":"Nguyen, H.H., David, C., Qin, S.C., Chin, W.-N.: Automated verification of shape and size properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 251\u2013266. Springer, Heidelberg (2007)"},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and Information Hiding. In: ACM POPL, Venice, Italy (January 2004)","DOI":"10.1145\/964001.964024"},{"key":"29_CR19","unstructured":"Pientka, B.: A heuristic for case analysis. Technical report (1995)"},{"key":"29_CR20","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"8","author":"W. Pugh","year":"1992","unstructured":"Pugh, W.: The Omega Test: A fast practical integer programming algorithm for dependence analysis. Communications of the ACM\u00a08, 102\u2013114 (1992)","journal-title":"Communications of the ACM"},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: IEEE LICS, Copenhagen, Denmark, pp. 55\u201374 (July 2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"Seino, T., Ogato, K., Futatsugi, K.: Mechanically supporting case analysis for verification of distributed systems. In: IJPCC (2005)","DOI":"10.1108\/17427370580000119"},{"key":"29_CR23","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1145\/1542476.1542514","volume-title":"PLDI","author":"K. Zee","year":"2009","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: An integrated proof language for imperative programs. In: PLDI, pp. 338\u2013351. ACM, New York (2009)"}],"container-title":["Lecture Notes in Computer Science","FM 2011: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21437-0_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T00:07:20Z","timestamp":1560298040000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21437-0_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214363","9783642214370"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21437-0_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}