{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T10:48:56Z","timestamp":1725792536610},"publisher-location":"Cham","reference-count":10,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319061993"},{"type":"electronic","value":"9783319062006"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06200-6_29","type":"book-chapter","created":{"date-parts":[[2014,4,23]],"date-time":"2014-04-23T05:53:48Z","timestamp":1398232428000},"page":"343-358","source":"Crossref","is-referenced-by-count":6,"title":["Formal Verification of kLIBC with the WP Frama-C Plug-in"],"prefix":"10.1007","author":[{"given":"Nuno","family":"Carvalho","sequence":"first","affiliation":[]},{"given":"Cristiano","family":"da Silva Sousa","sequence":"additional","affiliation":[]},{"given":"Jorge Sousa","family":"Pinto","sequence":"additional","affiliation":[]},{"given":"Aaron","family":"Tomb","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Meyer, B.: Applying \u201cDesign by Contract\u201d. IEEE Computer\u00a025(10) (1992)","DOI":"10.1109\/2.161279"},{"key":"29_CR2","unstructured":"Burghardt, J., Carben, A., Gerlach, J., Hartig, K., Pohl, H., V\u00f6llinger, K.: ACSL By Example \u2013 Towards a Verified C Standard Library. DEVICE-SOFT project publication. Fraunhofer FIRST Institute (2011)"},{"key":"29_CR3","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language (June 2013)"},{"issue":"3","key":"29_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2187671.2187678","volume":"44","author":"J. Hatcliff","year":"2012","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv.\u00a044(3), 16:1\u201316:58 (2012)","journal-title":"ACM Comput. Surv."},{"key":"29_CR5","unstructured":"Leavens, G., Cheon, Y.: Design by Contract with JML (2003)"},{"key":"29_CR6","unstructured":"Correnson, L., Cuoq, P., Kirchner, F., Prevosto, V., Puccetti, A., Signoles, J., Yakobowski, B.: Frama-C User Manual (June 2013)"},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"March\u00e9, C.: Jessie: An Intermediate Language for Java and C Verification. In: Stump, A., Xi, H. (eds.) Proceedings of PLPV 2007. ACM (2007)","DOI":"10.1145\/1292597.1292598"},{"key":"29_CR8","unstructured":"Baudin, P., Correnson, L., Dargaye, Z.: WP Plug-in Manual (June 2013)"},{"key":"29_CR9","unstructured":"Baudin, P., Correnson, L., Hermann, P.: WP Tutorial (September 2012)"},{"key":"29_CR10","unstructured":"Hermann, P., Signoles, J.: Frama-C\u2019s annotation generator plug-in (June 2013)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06200-6_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T17:27:09Z","timestamp":1558891629000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06200-6_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319061993","9783319062006"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06200-6_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}