{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T18:35:39Z","timestamp":1761676539583,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661964"},{"type":"electronic","value":"9783319661971"}],"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-66197-1_2","type":"book-chapter","created":{"date-parts":[[2017,8,11]],"date-time":"2017-08-11T21:02:30Z","timestamp":1502485350000},"page":"17-34","source":"Crossref","is-referenced-by-count":7,"title":["Focused Certification of an Industrial Compilation and Static Verification Toolchain"],"prefix":"10.1007","author":[{"given":"Zhi","family":"Zhang","sequence":"first","affiliation":[]},{"family":"Robby","sequence":"additional","affiliation":[]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[]},{"given":"Yannick","family":"Moy","sequence":"additional","affiliation":[]},{"given":"Pierre","family":"Courtieu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,13]]},"reference":[{"key":"2_CR1","unstructured":"Barnes, J.: SPARK: The Proven Approach to High Integrity Software. Altran Praxis (2012)"},{"key":"2_CR2","volume-title":"Ada 2012 Rationale - The Language, The Standard Libraries, Lecture Notes in Computer Science","author":"J Barnes","year":"2013","unstructured":"Barnes, J.: Ada 2012 Rationale - The Language, The Standard Libraries, Lecture Notes in Computer Science, vol. 8338. Springer, Heidelberg (2013)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-20398-5_6","volume-title":"NASA Formal Methods","author":"J Belt","year":"2011","unstructured":"Belt, J., Hatcliff, J., Robby, Chalin, P., Hardin, D., Deng, X.: Bakar kiasan: flexible contract checking for critical systems using symbolic execution. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 58\u201372. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-20398-5_6"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-25032-3_2","volume-title":"Formal Methods, Foundations and Applications","author":"R Chapman","year":"2011","unstructured":"Chapman, R., Botcazou, E., Wallenburg, A.: SPARKSkein: a formal and fast reference implementation of skein. In: Simao, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol. 7021, pp. 16\u201327. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-25032-3_2"},{"key":"2_CR5","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Courtieu, P., Aponte, M., Crolard, T., Zhang, Z., Robby, Belt, J., Hatcliff, J., Guitton, J., Jennings, T.: Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq. In: HILT, pp. 21\u201322 (2013)","DOI":"10.1145\/2658982.2527278"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"Patrick Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The astre\u00e9 analyzer. In: ESOP, pp. 21\u201330 (2005)"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Wassyng, A., Kelly, T., Comar, C., Jones, P.L.: Certifiably safe software-dependent systems: challenges and directions. In: FOSE, pp. 182\u2013200 (2014)","DOI":"10.1145\/2593882.2593895"},{"issue":"1","key":"2_CR10","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1145\/2775051.2676966","volume":"50","author":"Jacques-Henri Jourdan","year":"2015","unstructured":"Jourdan, J., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL, pp. 247\u2013259 (2015)","journal-title":"ACM SIGPLAN Notices"},{"issue":"7","key":"2_CR11","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"2_CR12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139629294","volume-title":"Building High Integrity Applications with SPARK","author":"JW McCormick","year":"2015","unstructured":"McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press, Cambridge (2015)"},{"issue":"3","key":"2_CR13","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1109\/MS.2013.43","volume":"30","author":"Yannick Moy","year":"2013","unstructured":"Moy, Y., Ledinot, E., Delseny, H., Wiels, V., Monate, B.: Testing or formal verification: DO-178C alternatives and industrial experience. IEEE Software, pp. 50\u201356 (2013)","journal-title":"IEEE Software"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"O\u2019Neill, I.: SPARK - a language and tool-set for high-integrity software development. In: Industrial Use of Formal Methods: Formal Verification. Wiley (2012)","DOI":"10.1002\/9781118561829.ch1"},{"key":"2_CR16","unstructured":"Ada conformity assessment test suite (ACATS). http:\/\/www.ada-auth.org\/acats.html"},{"key":"2_CR17","unstructured":"Ada reference manual. http:\/\/www.ada-auth.org\/standards\/ada12.html"},{"key":"2_CR18","unstructured":"Clight. http:\/\/compcert.inria.fr\/doc\/html\/Clight.html"},{"key":"2_CR19","unstructured":"Compcert-c. http:\/\/compcert.inria.fr\/compcert-C.html"},{"key":"2_CR20","unstructured":"The Coq proof assistant. http:\/\/coq.inria.fr"},{"key":"2_CR21","unstructured":"SPARK 2014 reference manual. http:\/\/docs.adacore.com\/spark2014-docs\/html\/lrm\/"},{"key":"2_CR22","unstructured":"Why3 - where programs meet provers. http:\/\/why3.lri.fr\/"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66197-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T06:02:49Z","timestamp":1569996169000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66197-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661964","9783319661971"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66197-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}