{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:47:10Z","timestamp":1725540430865},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642050886"},{"type":"electronic","value":"9783642050893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_27","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T22:31:40Z","timestamp":1257287500000},"page":"419-434","source":"Crossref","is-referenced-by-count":5,"title":["Certifiable Specification and Verification of C Programs"],"prefix":"10.1007","author":[{"given":"Christoph","family":"L\u00fcth","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dennis","family":"Walter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P. Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 342\u2013363. Springer, Heidelberg (2006)"},{"unstructured":"Baudin, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI C specification language. (October 2008), Preliminary design, version 1.4, http:\/\/frama-c.cea.fr\/download\/acsl_1.4.pdf","key":"27_CR2"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"27_CR4","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/978-94-010-0413-8_11","volume-title":"Proof and System-Reliability","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics in Isabelle\/HOL. In: Schwichtenberg, H., Steinbr\u00fcggen, R. (eds.) Proof and System-Reliability, pp. 341\u2013367. Kluwer, Dordrecht (2002)"},{"doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","key":"27_CR5","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"27_CR6","series-title":"Foundations of Computing Series","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"G. Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages. Foundations of Computing Series. MIT Press, Cambridge (1993)"},{"unstructured":"Programming languages \u2014 C. ISO\/IEC Standard 9899:1999(E), 2nd edn. (1999)","key":"27_CR7"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/10722010_8","volume-title":"Mathematics of Program Construction","author":"R. Bornat","year":"2000","unstructured":"Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 102\u2013126. Springer, Heidelberg (2000)"},{"unstructured":"MISRA-C: 2004. Guidelines for the use of the C language in critical systems (2004)","key":"27_CR9"},{"issue":"1","key":"27_CR10","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Information and Computation\u00a093(1), 55\u201392 (1991)","journal-title":"Information and Computation"},{"key":"27_CR11","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/781131.781153","volume-title":"Proc. PLDI 2003","author":"B. Blanchet","year":"2003","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proc. PLDI 2003, San Diego, California, USA, pp. 196\u2013207. ACM Press, New York (2003)"},{"issue":"10","key":"27_CR12","doi-asserted-by":"publisher","first-page":"785","DOI":"10.1109\/32.469460","volume":"21","author":"A. Borgida","year":"1995","unstructured":"Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Transactions on Software Engineering\u00a021(10), 785\u2013798 (1995)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"27_CR15","first-page":"193","volume-title":"Proc. POPL 2001","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: Proc. POPL 2001, pp. 193\u2013205. ACM Press, New York (2001)"},{"unstructured":"Frese, U., Hausmann, D., L\u00fcth, C., T\u00e4ubig, H., Walter, D.: The importance of being formal. In: Hungar, H. (ed.) Int. Workshop on the Certification of Safety-Critical Software Controlled Systems, SafeCert 2008. To appear in Electronic Notes in Theoretical Computer Science (2008)","key":"27_CR16"},{"unstructured":"Frama-C (2008), http:\/\/frama-c.cea.fr\/","key":"27_CR17"},{"issue":"4","key":"27_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/1278901.1278904","volume":"41","author":"G. Heiser","year":"2007","unstructured":"Heiser, G., Elphinstone, K., Kuz, I., Klein, G., Petters, S.M.: Towards trustworthy computing systems: Taking microkernels to the next level. ACM Operating Systems Review\u00a041(4), 3\u201311 (2007)","journal-title":"ACM Operating Systems Review"},{"unstructured":"The VeriSoft project, http:\/\/www.verisoft.de\/","key":"27_CR19"},{"key":"27_CR20","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1145\/336512.336546","volume-title":"ICSE 2000: Proc. of the Conference on The Future of Software Engineering","author":"A. Lamsweerde van","year":"2000","unstructured":"van Lamsweerde, A.: Formal specification: a roadmap. In: ICSE 2000: Proc. of the Conference on The Future of Software Engineering, pp. 147\u2013159. ACM, New York (2000)"},{"issue":"2","key":"27_CR21","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1145\/1057387.1057391","volume":"27","author":"T. Ball","year":"2005","unstructured":"Ball, T., Millstein, T., Rajamani, S.K.: Polymorphic predicate abstraction. ACM TOPLAS\u00a027(2), 314\u2013343 (2005)","journal-title":"ACM TOPLAS"},{"unstructured":"Norrish, M.: C Formalised in HOL. PhD thesis, University of Cambridge (1998)","key":"27_CR22"}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:35Z","timestamp":1606186055000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}