Keynote by Dimitra Giannakopoulou
"Fly me to the moon": Verification of Aerospace Systems
Date: Wednesday September 15th Time: 9.00 - 10.00
The safety-critical nature of Aerospace Systems mandates the development of advanced formal verification techniques that provide desired correctness guarantees.
In this talk, we will discuss two inherently different approaches towards achieving this goal.
The first approach aims at scaling exhaustive verification techniques by applying divide-and-conquer principles. It involves automated compositional verification algorithms for model checking both finite and infinite-state software components.
The second approach does not perform exhaustive verification but it is more versatile. It uses a model checker to automatically generate tests for aerospace algorithms and only requires knowledge of the types of inputs that the algorithms process.
We will discuss our experience with formal verification of aerospace systems and analyze the applicability of the two approaches in several settings.Sponsored by FME