The failure or malfunction of safety-critical aerospace, healthcare, power generation, and transportation systems can have catastrophic consequences for human beings and the environment. This makes it necessary to verify and validate such critical systems in order to guarantee their safe operation. Formal methods can facilitate the rigorous verification of such systems by using mathematical techniques to reason about the properties of the underlying hardware and software components. The ASSURE research program aims to employ formal methods-based techniques for the verification of safety-critical systems and their correctness properties.
More details about our research can be found in the dedicated milestone pages.
Milestones:
Formally Verified Decentralized Air Traffic Management
Formal Verification of Dynamic Data-Driven Aerospace Systems
Publications:
Open Source Software:
- A proof library in Athena for reasoning about probabilistic properties of distributed systems
- A proof library in Agda for flight safety envelopes with runtime monitors