Sciweavers

Share
EMSOFT
2007
Springer

Proving the absence of run-time errors in safety-critical avionics code

9 years 6 months ago
Proving the absence of run-time errors in safety-critical avionics code
We explain the design of the interpretation-based static analyzer Astr´ee and its use to prove the absence of run-time errors in safety-critical codes. Categories and Subject Descriptors D.2.4 [Software]: Software Engineering—Software/Program Verification; F.3.1, F.3.2 [Theory of Computation]: Logics and Meanings of Programs—Specifying and Verifying and Reasoning about Programs, Semantics of Programming Languages General Terms Reliability, Languages, Verification Software engineering has focussed on methods for designing larger and larger computer applications but software quality has not followed this dramatic progression. Poor software quality is not acceptable in safety and mission critical applications. An avenue is therefore opened for formal methods which are product-based (as opposed to development process-based). Abstract interpretation [3, 5] is a formal method for software verification which is having significant industrial applications, in particular in the context ...
Patrick Cousot
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where EMSOFT
Authors Patrick Cousot
Comments (0)
books