Static analysis and verification of aerospace software by abstract interpretation

Julien Bertrane; Patrick Cousot; Radhia Cousot; Jérôme Feret; Laurent Mauborgne; Antoine Miné; Xavier Rival

doi:10.1561/2500000002

Static analysis and verification of aerospace software by abstract interpretation

Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

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.

Original language	English (US)
Pages (from-to)	71-190
Number of pages	120
Journal	Foundations and Trends in Programming Languages
Volume	2
Issue number	2-3
DOIs	https://doi.org/10.1561/2500000002
State	Published - 2015

ASJC Scopus subject areas

Software
Theoretical Computer Science
Computer Science Applications

Access to Document

10.1561/2500000002

Cite this

@article{2eb460e296ee4064bb3911cb8a9bfd57,

title = "Static analysis and verification of aerospace software by abstract interpretation",

abstract = "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.",

author = "Julien Bertrane and Patrick Cousot and Radhia Cousot and J{\'e}r{\^o}me Feret and Laurent Mauborgne and Antoine Min{\'e} and Xavier Rival",

note = "Publisher Copyright: {\textcopyright} 2015 J. Bertrane et al.",

year = "2015",

doi = "10.1561/2500000002",

language = "English (US)",

volume = "2",

pages = "71--190",

journal = "Foundations and Trends in Programming Languages",

issn = "2325-1107",

publisher = "Now Publishers Inc",

number = "2-3",

}

TY - JOUR

T1 - Static analysis and verification of aerospace software by abstract interpretation

AU - Bertrane, Julien

AU - Cousot, Patrick

AU - Cousot, Radhia

AU - Feret, Jérôme

AU - Mauborgne, Laurent

AU - Miné, Antoine

AU - Rival, Xavier

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84996503516&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84996503516&partnerID=8YFLogxK

U2 - 10.1561/2500000002

DO - 10.1561/2500000002

M3 - Article

AN - SCOPUS:84996503516

SN - 2325-1107

VL - 2

SP - 71

EP - 190

JO - Foundations and Trends in Programming Languages

JF - Foundations and Trends in Programming Languages

IS - 2-3

ER -

Static analysis and verification of aerospace software by abstract interpretation

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this