{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:08Z","timestamp":1762458548883},"publisher-location":"Berlin, Heidelberg","reference-count":5,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_27","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T05:31:33Z","timestamp":1188451893000},"page":"385-390","source":"Crossref","is-referenced-by-count":7,"title":["KeY-C: A Tool for Verification of C Programs"],"prefix":"10.1007","author":[{"given":"Oleg","family":"M\u00fcrk","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Larsson","sequence":"additional","affiliation":[]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/11576280_22","volume-title":"Formal Methods and Software Engineering","author":"B. Beckert","year":"2005","unstructured":"Beckert, B., Schlager, S., Schmitt, P.H.: An improved rule for while loops in deductive program verification. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, pp. 315\u2013329. Springer, Heidelberg (2005)"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"539","DOI":"10.1007\/978-3-540-24644-2_35","volume-title":"Languages and Compilers for Parallel Computing","author":"S.I. Lee","year":"2004","unstructured":"Lee, S.I., Johnson, T.A., Eigenmann, R.: Cetus\u2014an extensible compiler infrastructure for source-to-source transformation. In: Rauchwerger, L. (ed.) LCPC 2003. LNCS, vol.\u00a02958, pp. 539\u2013553. Springer, Heidelberg (2004)"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","DOI":"10.1007\/978-3-540-32275-7_26"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T05:53:07Z","timestamp":1619502787000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":5,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}