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

• Type: Conference
• Year: 2007
• Where: EMSOFT
• Authors: Patrick Cousot
• Keywords: EMSOFT 2007, Interpretation-based Static Analyzer, Software, Static Analyzer