{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:40Z","timestamp":1775873680622,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642050886","type":"print"},{"value":"9783642050893","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_34","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T22:31:40Z","timestamp":1257287500000},"page":"532-546","source":"Crossref","is-referenced-by-count":55,"title":["Formal Verification of Avionics Software Products"],"prefix":"10.1007","author":[{"given":"Jean","family":"Souyris","sequence":"first","affiliation":[]},{"given":"Virginie","family":"Wiels","sequence":"additional","affiliation":[]},{"given":"David","family":"Delmas","sequence":"additional","affiliation":[]},{"given":"Herv\u00e9","family":"Delseny","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"34_CR1","unstructured":"The ASTREE project (Analyse Statique de logiciels Temps-REel Embarqu\u00e9s). RNTL (2003), \n                    \n                      http:\/\/www.di.ens.fr\/~cousot\/projets\/ASTREE\/"},{"key":"34_CR2","unstructured":"The CAT project (C analysis toolbox). RNTL (2005)"},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTR\u00c9E analyser. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"34_CR4","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-1-4020-8157-6_27","volume-title":"Building the Information Society","author":"P. Cousot","year":"2004","unstructured":"Cousot, P., Cousot, R.: Basic Concepts of Abstract Interpretation. In: Jacquard, R. (ed.) Building the Information Society, pp. 359\u2013366. Kluwer Academic Publishers, Dordrecht (2004)"},{"key":"34_CR5","unstructured":"DAEDALUS project. IST-1999-20527 of the european IST Programme of the Fifth Framework Programme (FP5) on the \u00ab\u00a0validation of software components embedded in future generation critical concurrent systems by exhaustive semantic-based static analysis and abstract testing methods based on abstract interpretation\u00a0\u00bb (DAEDALUS lasted from October 1st, 2000 to September 30th 2002)"},{"key":"34_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-642-04570-7_6","volume-title":"FMICS 2009","author":"D. Delmas","year":"2009","unstructured":"Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., V\u00e9drine, F.: Towards an industrial use of FLUCTUAT on safety-critical avionics software. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol.\u00a05825, pp. 53\u201369. Springer, Heidelberg (2009)"},{"key":"34_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/978-3-540-74061-2_27","volume-title":"Static Analysis","author":"D. Delmas","year":"2007","unstructured":"Delmas, D., Souyris, J.: ASTR\u00c9E: From research to industry. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 437\u2013451. Springer, Heidelberg (2007)"},{"key":"34_CR8","volume-title":"A discipline of programming; automatic Computation","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A discipline of programming; automatic Computation. Prentice Hall Int., Englewood Cliffs (1976)"},{"key":"34_CR9","unstructured":"DO-178B\/ED-12B. Software Considerations in Airborne Systems and Equipment Certification. RTCA\/EUROCAE (1992)"},{"key":"34_CR10","unstructured":"Duprat, S., Souyris, J., Favre-F\u00e9lix, D.: Formal verification workbench for avionics software. In: SIA (ed.) European Congress ERTS 2006 (European Real Time Software). R-2006-01-2A2 (2006)"},{"key":"34_CR11","unstructured":"ES_PASS project. ITEA 2 06042 (October 2007), \n                    \n                      http:\/\/www.itea2.org\/public\/project_leaflets\/ES_PASS_profile_oct-07.pdf"},{"key":"34_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/3-540-45449-7_32","volume-title":"Embedded Software","author":"C. Ferdinand","year":"2001","unstructured":"Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., Wilhelm, R.: Reliable and precise WCET determination for a real life processor. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol.\u00a02211, pp. 469\u2013485. Springer, Heidelberg (2001)"},{"key":"34_CR13","unstructured":"Hayhurst, K.J., Veerhusen, D.S., Chilenski, J.J., Rierson, L.K.: A practical tutorial on Modified Condition\/Decision Coverage. NASA\/TM-2001-210876 (2001)"},{"key":"34_CR14","unstructured":"Frama-C, \n                    \n                      http:\/\/frama-c.cea.fr\/"},{"key":"34_CR15","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communication of the ACM\u00a012(10) (October 1969)","DOI":"10.1145\/363235.363259"},{"key":"34_CR16","unstructured":"The Institute of Electrical and Inc Electronics Engineers. IEEE standard for binary floating-point arithmetic. Technical Report ANSI\/IEEE Std 745. IEEE Computer Society, Los Alamitos (1985)"},{"key":"34_CR17","unstructured":"Leroy, X.: The Compcert verified compiler, software and commented proof (August 2008), \n                    \n                      http:\/\/compcert.inria.fr\/"},{"key":"34_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1798","DOI":"10.1007\/3-540-48118-4_45","volume-title":"FM\u201999 - Formal Methods","author":"F. Randimbivololona","year":"1999","unstructured":"Randimbivololona, F., Souyris, J., Baudin, P., Pacalet, A., Raguideau, J., Schoen, D.: Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol.\u00a01709, pp. 1798\u20131815. Springer, Heidelberg (1999)"},{"key":"34_CR19","volume-title":"31st Symposium on Principles of Programming Languages (POPL 2004)","author":"X. Rival","year":"2004","unstructured":"Rival, X.: Symbolic Transfer Functions-based Approaches to Certified Compilation. In: 31st Symposium on Principles of Programming Languages (POPL 2004), Venice. ACM, New York (2004)"},{"key":"34_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-540-75101-4_45","volume-title":"Computer Safety, Reliability, and Security","author":"J. Souyris","year":"2007","unstructured":"Souyris, J., Delmas, D.: Experimental assessment of astr\u00e9e on safety-critical avionics software. In: Saglietti, F., Oster, N. (eds.) SAFECOMP 2007. LNCS, vol.\u00a04680, pp. 479\u2013490. Springer, Heidelberg (2007)"},{"key":"34_CR21","doi-asserted-by":"crossref","unstructured":"Souyris, J., Favre-Felix, D.: Proof of properties in avionics. In: IFIP Congress Topical Sessions 2004, pp. 527\u2013536 (2004)","DOI":"10.1007\/978-1-4020-8157-6_48"},{"key":"34_CR22","unstructured":"Souyris, J., Le Pavec, E., Himbert, G., J\u00e9gu, V., Borios, G., Heckmann, R.: Computing the worst case execution time of an avionics program by abstract interpretation. In: 5th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, pp. 21\u201324 (2005)"},{"key":"34_CR23","unstructured":"Stackanalyzer, \n                    \n                      http:\/\/www.absint.com\/stackanalyzer\/"},{"key":"34_CR24","unstructured":"Projet 2005 TH\u00c9S\u00c9E du RNTL (R\u00e9seau National des Technologies Logicielles) de l\u2019ANR"},{"key":"34_CR25","unstructured":"Projet 2008 U3CAT de l\u2019Agence nationale de la recherche (ANR)"}],"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_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:19:04Z","timestamp":1619781544000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}