{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T04:04:01Z","timestamp":1725595441239},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642226724"},{"type":"electronic","value":"9783642226731"}],"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-22673-1_28","type":"book-chapter","created":{"date-parts":[[2011,7,13]],"date-time":"2011-07-13T07:49:15Z","timestamp":1310543355000},"page":"301-303","source":"Crossref","is-referenced-by-count":6,"title":["A Formalization of the C99 Standard in HOL, Isabelle and Coq"],"prefix":"10.1007","author":[{"given":"Robbert","family":"Krebbers","sequence":"first","affiliation":[]},{"given":"Freek","family":"Wiedijk","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"28_CR1","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/1646353.1646374","volume":"53","author":"A. Bessey","year":"2010","unstructured":"Bessey, A., et al.: A few billion lines of code later: using static analysis to find bugs in the real world. Communications of the ACM\u00a053(2), 66\u201375 (2010)","journal-title":"Communications of the ACM"},{"issue":"3","key":"28_CR2","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","volume":"43","author":"S. Blazy","year":"2009","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning\u00a043(3), 263\u2013288 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"28_CR3","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":"28_CR4","unstructured":"Coq Development Team. The Coq Proof Assistant Reference Manual (2010)"},{"key":"28_CR5","unstructured":"International\u00a0Organization for Standardization. ISO\/IEC 9899: Programming languages \u2013 C. ISO Working Group 14 (1999), Draft standard WG14\/N1256, the combined C99 + TC1 + TC2 + TC3 (September 7, 2007)"},{"key":"28_CR6","unstructured":"Foundations Group of the ICIS. Research\/MathWiki, \n                    \n                      http:\/\/www.fnds.cs.ru.nl\/fndswiki\/Research\/MathWiki"},{"volume-title":"Introduction to HOL","year":"1993","key":"28_CR7","unstructured":"Gordon, M., Melham, T. (eds.): Introduction to HOL. Cambridge University Press, Cambridge (1993)"},{"key":"28_CR8","volume-title":"The C Programming Language","author":"B.W. Kernighan","year":"1988","unstructured":"Kernighan, B.W., Ritchie, D.M.: The C Programming Language, 2nd edn. Prentice Hall, Englewood Cliffs (1988)","edition":"2"},{"key":"28_CR9","unstructured":"LangPop.com. Programming Language Popularity, \n                    \n                      http:\/\/langpop.com\/"},{"key":"28_CR10","unstructured":"Moy, Y., March\u00e9, C.: Jessie Plugin Tutorial, Beryllium version. INRIA (2009)"},{"key":"28_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M. (eds.): Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"1","key":"28_CR12","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1017\/S0956796809990293","volume":"20","author":"P. Sewell","year":"2010","unstructured":"Sewell, P., et al.: Ott: Effective tool support for the working semanticist. Journal of Functional Programming\u00a020(1), 70\u2013122 (2010)","journal-title":"Journal of Functional Programming"},{"key":"28_CR13","unstructured":"TIOBE Software. TIOBE Programming Community index, \n                    \n                      http:\/\/www.tiobe.com\/content\/paperinfo\/tpci\/"},{"key":"28_CR14","unstructured":"Wiedijk, F.: Formalizing the C99 standard in HOL, Isabelle and Coq (2010), \n                    \n                      http:\/\/www.cs.ru.nl\/~freek\/notes\/ch2o.pdf"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22673-1_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,29]],"date-time":"2019-03-29T21:45:16Z","timestamp":1553895916000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22673-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642226724","9783642226731"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22673-1_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}