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

摘要

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