{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T14:52:45Z","timestamp":1774795965601,"version":"3.50.1"},"reference-count":90,"publisher":"Emerald","issue":"2-3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,12,15]]},"abstract":"<jats:p>We discuss the principles of static analysis by abstract interpretation and report on the automatic verification of the absence of runtime errors in large embedded aerospace software by static analysis based on abstract interpretation. The first industrial applications concerned synchronous control\/command software in open loop. Recent advances consider imperfectly synchronous programs, parallel programs, and target code validation as well. Future research directions on abstract interpretation are also discussed in the context of aerospace software.<\/jats:p>","DOI":"10.1561\/2500000002","type":"journal-article","created":{"date-parts":[[2015,12,15]],"date-time":"2015-12-15T05:50:30Z","timestamp":1450158630000},"page":"71-190","source":"Crossref","is-referenced-by-count":31,"title":["Static Analysis and Verification of Aerospace Software by Abstract Interpretation"],"prefix":"10.1561","volume":"2","author":[{"given":"Julien","family":"Bertrane","sequence":"first","affiliation":[{"name":"\u00c9cole normale sup\u00e9rieure D\u00e9partement d\u2019informatique,"}]},{"given":"Patrick","family":"Cousot","sequence":"additional","affiliation":[{"name":"New York University D\u00e9partement d\u2019informatique, \u00c9cole normale sup\u00e9rieure & Courant Institute of Mathematical Sciences,"}]},{"given":"Radhia","family":"Cousot","sequence":"additional","affiliation":[{"name":"\u00c9cole normale sup\u00e9rieure CNRS & D\u00e9partement d\u2019informatique,"}]},{"given":"J\u00e9r\u00f4me","family":"Feret","sequence":"additional","affiliation":[{"name":"\u00c9cole normale sup\u00e9rieure INRIA & D\u00e9partement d\u2019informatique,"}]},{"given":"Laurent","family":"Mauborgne","sequence":"additional","affiliation":[{"name":"AbsInt Angewandte Informatik"}]},{"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[{"name":"Sorbonne University, University Pierre and Marie Curie , CNRS, LIP6"}]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[{"name":"\u00c9cole normale sup\u00e9rieure INRIA & D\u00e9partement d\u2019informatique,"}]}],"member":"140","published-online":{"date-parts":[[2015,12,15]]},"reference":[{"key":"2026032910221756000_ref001","unstructured":"AbsInt\n          , Angewandte Informatik. Astr\u00e9e run-time error analyzer. http:\/\/www.absint.com\/astree\/."},{"key":"2026032910221756000_ref002","unstructured":"Aeronautical Radio, Inc. (ARINC)\n          . ARINC 653. http:\/\/www.arinc.com\/."},{"key":"2026032910221756000_ref003","first-page":"97","volume-title":"Static analysis by abstract interpretation of the quasi-synchronous composition of synchronous programs","author":"Bertrane","year":"2005"},{"key":"2026032910221756000_ref004","first-page":"370","volume-title":"Proving the properties of communicating imperfectly-clocked synchronous systems","author":"Bertrane","year":"2006"},{"key":"2026032910221756000_ref005","first-page":"1","volume-title":"AIAA Infotech@Aerospace (I@A 2010)","author":"Bertrane","year":"2010"},{"key":"2026032910221756000_ref006","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/978-3-642-03829-7_8","volume-title":"Foundations of Security Analysis and Design V, FOSAD 2007\/2008\/2009 Tutorial Lectures, volume 5705 of LNCS","author":"Besson","year":"2009"},{"key":"2026032910221756000_ref007","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/3-540-36377-7_5","volume-title":"The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, volume 2566 of LNCS","author":"Blanchet","year":"2002"},{"key":"2026032910221756000_ref008","first-page":"196","volume-title":"A static analyzer for large safety-critical software","author":"Blanchet","year":"2003"},{"key":"2026032910221756000_ref009","first-page":"1","volume-title":"Space software validation using abstract interpretation","author":"Bouissou","year":"2009"},{"issue":"4","key":"2026032910221756000_ref010","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1017\/S0956796800000496","article-title":"Abstract interpretation by dynamic partitioning","volume":"2","author":"Bourdoncle","year":"1992","journal-title":"Journal of Functional Programming"},{"key":"2026032910221756000_ref011","first-page":"128","volume-title":"Efficient chaotic iteration strategies with widenings","author":"Bourdoncle","year":"1993"},{"issue":"8","key":"2026032910221756000_ref012","doi-asserted-by":"crossref","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for boolean function manipulation","volume":"C\u201335","author":"Bryant","year":"1986","journal-title":"IEEE Transactions on Computers"},{"key":"2026032910221756000_ref013","first-page":"308","volume-title":"Program proving as hand simulation with a little induction","author":"Burstall","year":"1974"},{"key":"2026032910221756000_ref014","first-page":"215","volume-title":"About the design of distributed control systems: The quasi-synchronous approach","author":"Caspi","year":"2001"},{"key":"2026032910221756000_ref015","volume-title":"M\u00e9thodes it\u00e9ratives de construction et d\u2019approximation de points fixes d\u2019op\u00e9rateurs monotones sur un treillis, analyse s\u00e9mantique de programmes (in French)","author":"Cousot","year":"1978"},{"key":"2026032910221756000_ref016","first-page":"303","volume-title":"Program Flow Analysis: Theory and Applications","author":"Cousot","year":"1981"},{"key":"2026032910221756000_ref017","first-page":"316","volume-title":"Types as abstract interpretations","author":"Cousot","year":"1997"},{"issue":"1","key":"2026032910221756000_ref018","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/S0304-3975(00)00313-3","article-title":"Constructive design of a hierarchy of semantics of a transition system by abstract interpretation","volume":"277","author":"Cousot","year":"2002","journal-title":"Theoretical Computer Science"},{"key":"2026032910221756000_ref019","first-page":"106","volume-title":"Static determination of dynamic properties of programs","author":"Cousot","year":"1976"},{"key":"2026032910221756000_ref020","first-page":"238","volume-title":"Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints","author":"Cousot","year":"1977"},{"issue":"1","key":"2026032910221756000_ref021","doi-asserted-by":"crossref","first-page":"43","DOI":"10.2140\/pjm.1979.82.43","article-title":"Constructive versions of Tarski\u2019s fixed point theorems","volume":"81","author":"Cousot","year":"1979","journal-title":"Pacific Journal of Mathematics"},{"key":"2026032910221756000_ref022","first-page":"269","volume-title":"Systematic design of program analysis frameworks","author":"Cousot","year":"1979"},{"key":"2026032910221756000_ref023","first-page":"243","volume-title":"Invariance proof methods and analysis techniques for parallel programs","author":"Cousot","year":"1984"},{"key":"2026032910221756000_ref024","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00290704","article-title":"Sometime = always + recursion \u2261 always: on the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs","volume":"24","author":"Cousot","year":"1987","journal-title":"Acta Informatica"},{"issue":"4","key":"2026032910221756000_ref025","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","article-title":"Abstract interpretation frameworks","volume":"2","author":"Cousot","year":"1992","journal-title":"Journal of Logic and Computation"},{"key":"2026032910221756000_ref026","first-page":"269","volume-title":"Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation","author":"Cousot","year":"1992"},{"key":"2026032910221756000_ref027","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0304-3975(93)90248-R","article-title":"\u201c\u00c0 la Burstall\u201d intermittent assertions induction principles for proving inevitability properties of programs","volume":"120","author":"Cousot","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"2026032910221756000_ref028","first-page":"178","volume-title":"Systematic design of program transformation frameworks by abstract interpretation","author":"Cousot","year":"2002"},{"key":"2026032910221756000_ref029","first-page":"84","volume-title":"Automatic discovery of linear restraints among variables of a program","author":"Cousot","year":"1978"},{"key":"2026032910221756000_ref030","volume-title":"The Astr\u00e9e static analyzer","author":"Cousot"},{"key":"2026032910221756000_ref031","first-page":"21","volume-title":"The Astr\u00e9e analyser","author":"Cousot","year":"2005"},{"key":"2026032910221756000_ref032","first-page":"272","volume-title":"Combination of abstractions in the Astr\u00e9e static analyzer","author":"Cousot","year":"2006"},{"key":"2026032910221756000_ref033","first-page":"3","volume-title":"Varieties of static analyzers: A comparison with Astr\u00e9e","author":"Cousot","year":"2007"},{"key":"2026032910221756000_ref034","first-page":"333","volume-title":"Fixpoint-guided abstraction refinements","author":"Cousot","year":"2007"},{"key":"2026032910221756000_ref035","first-page":"456","volume-title":"The reduced product of abstract domains and the combination of decision procedures","author":"Cousot","year":"2011"},{"key":"2026032910221756000_ref036","first-page":"437","volume-title":"Astr\u00e9e: from research to industry","author":"Delmas","year":"2007"},{"key":"2026032910221756000_ref037","first-page":"43","article-title":"Cooperating sequential processes","volume-title":"Programming Languages: NATO Advanced Study Institute","author":"Dijkstra","year":"1968"},{"key":"2026032910221756000_ref038","unstructured":"dSpace\n          . TargetLink code generator. http:\/\/www.dspaceinc.com."},{"key":"2026032910221756000_ref039","unstructured":"Esterel Technologies\n          . Scade suite\u2122, the standard for the development of safety-critical embedded software in the avionics industry. http:\/\/www.esterel-technologies.com\/."},{"key":"2026032910221756000_ref040","volume-title":"Elementa geometr\u00edas, book xii, proposition 17. fl. 300 BC","author":"Euclid of Alexandria"},{"key":"2026032910221756000_ref041","first-page":"33","volume-title":"Static analysis of digital filters","author":"Feret","year":"2004"},{"key":"2026032910221756000_ref042","first-page":"42","volume-title":"The arithmetic-geometric progression abstract domain","author":"Feret","year":"2005"},{"key":"2026032910221756000_ref043","volume-title":"Numerical abstract domains for digital filters","author":"Feret","year":"2005"},{"key":"2026032910221756000_ref044","first-page":"116","volume-title":"Static analysis via abstract interpretation of the happens-before memory model","author":"Ferrara","year":"2008"},{"key":"2026032910221756000_ref045","volume-title":"Static analysis via abstract interpretation of multithreaded programs","author":"Ferrara","year":"2009"},{"key":"2026032910221756000_ref046","first-page":"19","volume-title":"Assigning meanings to programs","author":"Floyd","year":"1967"},{"issue":"2","key":"2026032910221756000_ref047","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1145\/333979.333989","article-title":"Making abstract interpretations complete","volume":"47","author":"Giacobazzi","year":"2000","journal-title":"Journal of the Association for Computing Machinery"},{"key":"2026032910221756000_ref048","first-page":"89","volume-title":"Fourteen ways to fool your synchronizer","author":"Ginosar","year":"2003"},{"key":"2026032910221756000_ref049","volume-title":"The Java language specification","author":"Gosling","year":"2005","edition":"third"},{"key":"2026032910221756000_ref050","first-page":"234","volume-title":"Static analyses of floating-point operations","author":"Goubault","year":"2001"},{"issue":"3","key":"2026032910221756000_ref051","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1080\/00207168908803778","article-title":"Static analysis of arithmetical congruences","volume":"30","author":"Granger","year":"1989","journal-title":"International Journal of Computer Mathematics"},{"key":"2026032910221756000_ref052","first-page":"169","volume-title":"Static analysis of linear congruence equalities among variables of a program","author":"Granger","year":"1991"},{"key":"2026032910221756000_ref053","first-page":"26","volume-title":"Worst-case execution time prediction by static program analysis","author":"Heckmann","year":"2004"},{"key":"2026032910221756000_ref054","unstructured":"IEEE and The Open Group\n          . Portable operating system interface (POSIX). http:\/\/www.opengroup.org,http:\/\/standards.ieee.org."},{"key":"2026032910221756000_ref055","volume-title":"IEEE standard for binary floating-point arithmetic","author":"IEEE Computer Society","year":"1985"},{"key":"2026032910221756000_ref056","volume-title":"C standard. Technical Report 1124","author":"ISO\/IEC JTC1\/SC22\/WG14 Working Group.","year":"2007"},{"key":"2026032910221756000_ref057","volume-title":"Working draft, standard for programming language C++. Technical Report 3035","author":"ISO\/IEC JTC1\/SC22\/WG21 Working Group","year":"2010"},{"key":"2026032910221756000_ref058","unstructured":"B.\n              Jeannet\n             and A.Min\u00e9. The Apron numerical abstract domain library. http:\/\/apron.cri.ensmp.fr\/library\/,2007."},{"key":"2026032910221756000_ref059","first-page":"661","volume-title":"Apron: A library of numerical abstract domains for static analysis","author":"Jeannet","year":"2009"},{"key":"2026032910221756000_ref060","volume-title":"Development Methods for Computer Programs including a Notion of Interference","author":"Jones","year":"1981"},{"key":"2026032910221756000_ref061","first-page":"247","volume-title":"A formally-verified C static analyzer","author":"Jourdan","year":"2015"},{"key":"2026032910221756000_ref062","first-page":"1","volume-title":"Astr\u00e9e: Proving the absence of rutime errors","author":"K\u00e4stner","year":"2010"},{"issue":"2","key":"2026032910221756000_ref063","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","article-title":"Proving the correctness of multiprocess programs","volume":"3","author":"Lamport","year":"1977","journal-title":"IEEE Trans. on Software Engineering"},{"key":"2026032910221756000_ref064","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","article-title":"How to make a multiprocessor computer that correctly executes multiprocess programs","volume":"28","author":"Lamport","year":"1979","journal-title":"IEEE Transactions on Computers"},{"key":"2026032910221756000_ref065","first-page":"14","volume-title":"Efficient verification of realtime systems: Compact data structure and state-space reduction","author":"Larsen","year":"1997"},{"key":"2026032910221756000_ref066","first-page":"42","volume-title":"Formal certification of a compiler back-end or: programming a compiler with a proof assistant","author":"Leroy","year":"2006"},{"key":"2026032910221756000_ref067","first-page":"378","volume-title":"The java memory model","author":"Manson","year":"2005"},{"issue":"3","key":"2026032910221756000_ref068","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/s10703-009-0068-y","article-title":"Enhancing the implementation of mathematical formulas for fixed-point and floating-point arithmetics","volume":"35","author":"Martel","year":"2009","journal-title":"Formal Methods in System Design"},{"key":"2026032910221756000_ref069","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/978-1-4020-8157-6_30","volume-title":"Building the Information Society","author":"Mauborgne","year":"2004"},{"key":"2026032910221756000_ref070","first-page":"5","volume-title":"Trace partitioning in abstract interpretation based static analyzer","author":"Mauborgne","year":"2005"},{"key":"2026032910221756000_ref071","first-page":"310","volume-title":"The octagon abstract domain","author":"Min\u00e9","year":"2001"},{"key":"2026032910221756000_ref072","first-page":"3","volume-title":"Relational abstract domains for the detection of floating-point runtime errors","author":"Min\u00e9","year":"2004"},{"key":"2026032910221756000_ref073","volume-title":"Weakly Relational Numerical Abstract Domains","author":"Min\u00e9","year":"2004"},{"key":"2026032910221756000_ref074","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","article-title":"The octagon abstract domain","volume":"19","author":"Min\u00e9","year":"2006","journal-title":"Higher-Order and Symbolic Computation"},{"key":"2026032910221756000_ref075","first-page":"54","volume-title":"Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics","author":"Min\u00e9","year":"2006"},{"key":"2026032910221756000_ref076","first-page":"398","volume-title":"Static analysis of run-time errors in embedded critical parallel C programs","author":"Min\u00e9","year":"2011"},{"key":"2026032910221756000_ref077","first-page":"39","volume-title":"Relational thread-modular static value analysis by abstract interpretation","author":"Min\u00e9","year":"2014"},{"key":"2026032910221756000_ref078","first-page":"86","volume-title":"The parallel implementation of the Astr\u00e9e static analyzer","author":"Monniaux","year":"2005"},{"key":"2026032910221756000_ref079","volume-title":"Interval Analysis","author":"Moore","year":"1966"},{"key":"2026032910221756000_ref080","first-page":"106","volume-title":"Proof-Carrying Code","author":"Necula","year":"1997"},{"key":"2026032910221756000_ref081","first-page":"83","volume-title":"Translation Validation for an Optimizing Compiler","author":"Necula","year":"2000"},{"issue":"4","key":"2026032910221756000_ref082","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","article-title":"An axiomatic proof technique for parallel programs","volume":"6","author":"Owicki","year":"1976","journal-title":"Acta Informatica"},{"key":"2026032910221756000_ref083","first-page":"235","volume-title":"Translation Validation for Synchronous Languages","author":"Pnueli","year":"1998"},{"issue":"3","key":"2026032910221756000_ref084","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/BF01019459","article-title":"The discoveries of continuations","volume":"6","author":"Reynolds","year":"1993","journal-title":"Lisp and Sy, bolic Computation"},{"key":"2026032910221756000_ref085","first-page":"41","volume-title":"Abstract Interpretation-based Certification of Assembly Code","author":"Rival","year":"2003"},{"key":"2026032910221756000_ref086","first-page":"1","volume-title":"Symbolic transfer functions-based approaches to certified compilation","author":"Rival","year":"2004"},{"issue":"5","key":"2026032910221756000_ref087","doi-asserted-by":"crossref","DOI":"10.1145\/1275497.1275501","article-title":"The trace partitioning abstract domain","volume":"29","author":"Rival","year":"2007","journal-title":"ACM Transactions on Programming Languages Systems"},{"key":"2026032910221756000_ref088","first-page":"161","volume-title":"A theory of memory models","author":"Saraswat","year":"2007"},{"key":"2026032910221756000_ref089","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","article-title":"A lattice theoretical fixpoint theorem and its applications","volume":"5","author":"Tarski","year":"1955","journal-title":"Pacific Journal of Mathematics"},{"key":"2026032910221756000_ref090","volume-title":"DO\u2013178B. Technical report, Software Considerations in Airborne Systems and Equipment Certification","author":"Radio Technical Commission on Aviation","year":"1999"}],"container-title":["Foundations and Trends\u00ae in Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/2\/2-3\/71\/11025395\/2500000002en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/2\/2-3\/71\/11025395\/2500000002en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T14:22:35Z","timestamp":1774794155000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/ftpgl\/article\/2\/2-3\/71\/1326563\/Static-Analysis-and-Verification-of-Aerospace"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,15]]},"references-count":90,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2015,12,15]]}},"URL":"https:\/\/doi.org\/10.1561\/2500000002","relation":{},"ISSN":["2325-1107","2325-1131"],"issn-type":[{"value":"2325-1107","type":"print"},{"value":"2325-1131","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12,15]]}}}