We explain the design of the interpretation-based static analyzer AASTRÉE and its use to prove the absence of run-time errors in safety-critical codes.