{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T20:07:26Z","timestamp":1743106046936,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319035444"},{"type":"electronic","value":"9783319035451"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-03545-1_2","type":"book-chapter","created":{"date-parts":[[2013,12,9]],"date-time":"2013-12-09T16:31:48Z","timestamp":1386606708000},"page":"17-32","source":"Crossref","is-referenced-by-count":2,"title":["Mostly Sound Type System Improves a Foundational Program Verifier"],"prefix":"10.1007","author":[{"given":"Josiah","family":"Dodds","sequence":"first","affiliation":[]},{"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Appel, A.W.: Tactics for separation logic (2006)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"A.W. Appel","year":"2011","unstructured":"Appel, A.W.: Verified Software Toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 1\u201317. Springer, Heidelberg (2011)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-25379-9_18","volume-title":"Certified Programs and Proofs","author":"A.W. Appel","year":"2011","unstructured":"Appel, A.W.: VeriSmall: Verified Smallfoot shape analysis. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 231\u2013246. Springer, Heidelberg (2011)"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cambridge (to appear, 2014)","DOI":"10.1017\/CBO9781107256552"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-32347-8_21","volume-title":"Interactive Theorem Proving","author":"J. Bengtson","year":"2012","unstructured":"Bengtson, J., Jensen, J.B., Birkedal, L.: Charge! A framework for higher-order separation logic in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 315\u2013331. Springer, Heidelberg (2012)"},{"key":"2_CR6","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.\u00a03780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-35308-6_8","volume-title":"Certified Programs and Proofs","author":"B. Campbell","year":"2012","unstructured":"Campbell, B.: An executable semantics for compCert C. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol.\u00a07679, pp. 60\u201375. Springer, Heidelberg (2012)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Canet, G., Cuoq, P., Monate, B.: A value analysis for C programs. In: Ninth Source Code Analysis and Manipulation, pp. 123\u2013124. IEEE (2009)","DOI":"10.1109\/SCAM.2009.22"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI 2011, pp. 234\u2013245 (2011)","DOI":"10.1145\/1993316.1993526"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Reflection. In: Certified Programming With Dependent Types. MIT Press (2013)","DOI":"10.7551\/mitpress\/9153.001.0001"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P. Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol.\u00a07504, pp. 233\u2013247. Springer, Heidelberg (2012)"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Ellison, C., Ro\u015fu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th Symposium on Principles of Programming Languages (POPL 2012), pp. 533\u2013544. ACM (2012)","DOI":"10.1145\/2103656.2103719"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-32347-8_8","volume-title":"Interactive Theorem Proving","author":"D. Greenaway","year":"2012","unstructured":"Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: Automatic verified abstraction of C. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 99\u2013115. Springer, Heidelberg (2012)"},{"issue":"10","key":"2_CR15","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 578\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"2_CR16","unstructured":"Leroy, X.: The CompCert verified compiler, software and commented proof (June 2013), \n                      http:\/\/compcert.inria.fr"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-03359-9_24","volume-title":"Theorem Proving in Higher Order Logics","author":"A. McCreight","year":"2009","unstructured":"McCreight, A.: Practical tactics for separation logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 343\u2013358. Springer, Heidelberg (2009)"},{"key":"2_CR18","unstructured":"Norrish, M.: C-to-isabel parser (2013), \n                      http:\/\/www.ssrg.nicta.com.au\/software\/TS\/c-parser\/"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-642-03359-9_32","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Tuerk","year":"2009","unstructured":"Tuerk, T.: A formalisation of Smallfoot in HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 469\u2013484. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03545-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T21:52:20Z","timestamp":1676843540000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-03545-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319035444","9783319035451"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03545-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}