Static Analysis and Verification of Aerospace Software by Abstract Interpretation

We discuss the principles of static analysis by abstract interpretationand report on the automatic verification of the absence of runtimeerrors in large embedded aerospace software by static analysis basedon abstract interpretation. The first industrial applications concernedsynchronous control/command software in open loop. Recent advancesconsider imperfectly synchronous programs, parallel programs, and targetcode validation as well. Future research directions on abstract interpretationare also discussed in the context of aerospace software.

Domains

Performance [cs.PF] Embedded Systems

Fichier principal

article-bertrane-al-fntpl15.pdf (1.83 Mo)

Origin : Files produced by the author(s)

Antoine Miné : Connect in order to contact the contributor

https://hal.sorbonne-universite.fr/hal-01312241

Submitted on : Thursday, May 5, 2016-9:35:28 AM

Last modification on : Wednesday, October 4, 2023-3:38:53 AM

Long-term archiving on: Tuesday, November 15, 2016-8:30:19 PM

Dates and versions

hal-01312241 , version 1 (05-05-2016)

Identifiers

HAL Id : hal-01312241 , version 1
DOI : 10.1561/2500000002

Cite

Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, et al.. Static Analysis and Verification of Aerospace Software by Abstract Interpretation. Foundations and Trends in Programming Languages, 2015, 2 (2-3), pp.171-291. ⟨10.1561/2500000002⟩. ⟨hal-01312241⟩

Export

BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

ENS-PARIS UPMC UNIV-RENNES1 CNRS INRIA IRISA LIP6 INRIA2 PSL UR1-MATH-STIC UR1-UFR-ISTIC SORBONNE-UNIVERSITE SU-SCIENCES UR1-MATH-NUM

310 View

253 Download