{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:55:44Z","timestamp":1725558944016},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642142949"},{"type":"electronic","value":"9783642142956"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_28","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T18:36:09Z","timestamp":1278614169000},"page":"306-320","source":"Crossref","is-referenced-by-count":2,"title":["Verifying Low-Level Implementations of High-Level Datatypes"],"prefix":"10.1007","author":[{"given":"Christopher L.","family":"Conway","sequence":"first","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"28_CR1","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/90.222903","volume":"1","author":"M.B. Abbott","year":"1993","unstructured":"Abbott, M.B., Peterson, L.L.: A language-based approach to protocol implementation. IEEE\/ACM Trans. Netw.\u00a01(1), 4\u201319 (1993)","journal-title":"IEEE\/ACM Trans. Netw."},{"key":"28_CR2","unstructured":"American National Standard for Programming Languages - C, ANSI\/ISO 9899-1990 (August 1989)"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Bornat, R.: Proving pointer programs in Hoare logic. In: Mathematics of Program Construction, pp. 102\u2013126 (2000)","DOI":"10.1007\/10722010_8"},{"key":"28_CR4","unstructured":"Burstall, R.: Some techniques for proving correctness of programs which alter data structures. In: Machine Intelligence (1972)"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-540-69166-2_5","volume-title":"Static Analysis","author":"C.L. Conway","year":"2008","unstructured":"Conway, C.L., Dams, D., Namjoshi, K.S., Barrett, C.: Points-to analysis, conditional soundness, and proving the absence of errors. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol.\u00a05079, pp. 62\u201377. Springer, Heidelberg (2008)"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"CAV 2009","author":"Y. Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in Satisfiability Modulo Theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"key":"28_CR7","unstructured":"Hubert, T., March\u00e9, C.: Separation analysis for deductive verification. In: HAV, March 2007, pp. 81\u201393 (2007)"},{"issue":"3","key":"28_CR8","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/373243.375719","volume":"36","author":"S.S. Ishtiaq","year":"2001","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: Bi as an assertion language for mutable data structures. SIGPLAN Not.\u00a036(3), 14\u201326 (2001)","journal-title":"SIGPLAN Not."},{"issue":"4","key":"28_CR9","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/316194.316200","volume":"29","author":"E. Kohler","year":"1999","unstructured":"Kohler, E., Kaashoek, M.F., Montgomery, D.R.: A readable TCP in the Prolac protocol language. Computer Communication Review\u00a029(4), 3\u201313 (1999)","journal-title":"Computer Communication Review"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Landi, W., Ryder, B.G.: Pointer-induced aliasing: a problem taxonomy. In: POPL, January 1991, pp. 93\u2013103 (1991)","DOI":"10.1145\/99583.99599"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Landi, W., Ryder, B.G.: A safe approximate algorithm for interprocedural aliasing. In: Programming Language Design and Implementation (PLDI), June 1992, pp. 235\u2013248 (1992)","DOI":"10.1145\/143095.143137"},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"Laventhal, M.S.: Verifying programs which operate on data structures. In: Reliable Software, pp. 420\u2013426 (1975)","DOI":"10.1145\/800027.808465"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Madhavapeddy, A., Ho, A., Deegan, T., Scott, D., Sohan, R.: Melange: creating a \u201cfunctional\u201d internet. In: European Conf. on Comp. Sys. (EuroSys), pp. 101\u2013114 (2007)","DOI":"10.1145\/1272998.1273009"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"Mockapetris, P.: Domain names - implementation and specification. RFC 1035 (Standard) (November 1987)","DOI":"10.17487\/rfc1035"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"Oppen, D.C., Cook, S.A.: Proving assertions about programs that manipulate data structures. In: Symposium on the Theory of Computing (STOC), pp. 107\u2013116 (1975)","DOI":"10.1145\/800116.803758"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Pang, R., Paxson, V., Sommer, R., Peterson, L.: binpac: a yacc for writing application protocol parsers. In: Internet Measurement Conf. (IMC), pp. 289\u2013300 (2006)","DOI":"10.1145\/1177080.1177119"},{"key":"28_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-540-93900-9_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Z. Rakamaric","year":"2009","unstructured":"Rakamaric, Z., Hu, A.J.: A scalable memory model for low-level code. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 290\u2013304. Springer, Heidelberg (2009)"},{"key":"28_CR19","unstructured":"Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structure. In: Millenial Perspectives in Computer Science (2000)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14295-6_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:50:39Z","timestamp":1606168239000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}