{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:07:46Z","timestamp":1773655666459,"version":"3.50.1"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319671123","type":"print"},{"value":"9783319671130","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-67113-0_1","type":"book-chapter","created":{"date-parts":[[2017,8,24]],"date-time":"2017-08-24T00:21:24Z","timestamp":1503534084000},"page":"3-18","source":"Crossref","is-referenced-by-count":8,"title":["Deductive Functional Verification of Safety-Critical Embedded C-Code: An Experience Report"],"prefix":"10.1007","author":[{"given":"Dilian","family":"Gurov","sequence":"first","affiliation":[]},{"given":"Christian","family":"Lidstr\u00f6m","sequence":"additional","affiliation":[]},{"given":"Mattias","family":"Nyberg","sequence":"additional","affiliation":[]},{"given":"Jonas","family":"Westman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,25]]},"reference":[{"key":"1_CR1","unstructured":"Allocation Element Requirement AE417 Dual-Circuit Steering. Scania Technical Product Data (2015)"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-15057-9_3","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E Alkassar","year":"2010","unstructured":"Alkassar, E., Hillebrand, M.A., Paul, W., Petrova, E.: Automated verification of a small hypervisor. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 40\u201354. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-15057-9_3"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-04468-7_16","volume-title":"Computer Safety, Reliability, and Security","author":"C Baumann","year":"2009","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Formal verification of a microkernel used in dependable software systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) SAFECOMP 2009. LNCS, vol. 5775, pp. 187\u2013200. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-04468-7_16"},{"key":"1_CR4","unstructured":"Cohen, E.: Modular verification of hybrid system code with VCC. CoRR abs\/1403.3611 (2014)"},{"key":"1_CR5","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. 5674, pp. 23\u201342. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-03359-9_2"},{"key":"1_CR6","unstructured":"Cohen, E., Moskal, M., Schulte, W., Tobies, S.: A practical verification methodology for concurrent programs. Technical report MSR-TR-2009-15, Microsoft Research, February 2009"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Cohen, E., Moskal, M., Schulte, W., Tobies, S.: A precise yet efficient memory model for C. In: Workshop on Systems Software Verification (SSV 2009). Electronic Notes in Theoretical Computer Science, vol. 254, pp. 85\u2013103. Elsevier (2009)","DOI":"10.1016\/j.entcs.2009.09.061"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-33826-7_16"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Dordowsky, F.: An experimental study using ACSL and Frama-C to formulate and verify low-level requirements from a DO-178C compliant avionics project. In: Formal Integrated Development Environment (F-IDE 2015), pp. 28\u201341 (2015)","DOI":"10.4204\/EPTCS.187.3"},{"key":"1_CR10","unstructured":"Eriksson, J.: Formal Requirement Models for Automotive Embedded Systems. Master\u2019s thesis, KTH Royal Institute of Technology, School of Computer Science and Communication (2016)"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Gordon, M., Collavizza, H.: Forward with Hoare. In: Roscoe, A., Jones, C., Wood, K. (eds) Reflections on the Work of C.A.R. Hoare, pp. 101\u2013121. Springer, London (2010). doi:\n10.1007\/978-1-84882-912-1_5","DOI":"10.1007\/978-1-84882-912-1_5"},{"issue":"10","key":"1_CR12","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"1_CR13","unstructured":"Lidstr\u00f6m, C.: Verification of Functional Requirements of Embedded Automotive C Code. Master\u2019s thesis, KTH Royal Institute of Technology, School of Computer Science and Communication (2016)"}],"container-title":["Lecture Notes in Computer Science","Critical Systems: Formal Methods and Automated Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67113-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,10,19]],"date-time":"2017-10-19T02:34:30Z","timestamp":1508380470000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67113-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319671123","9783319671130"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67113-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}