Formal Methods 101: Formal Systems
Formal Methods 101: Decidability
Formal Methods 101: Complexity Theory
Formal Methods 101: Satisfiable Modulo Theories (SMT)
Formal Methods 101: Boolean Satisfiability (SAT)
Analysis of N-Queens Stochastic Algorithms Using Probabilistic Model Checking
Model-Based Design of a Closed-Loop Speed Controller for a Hybrid System
Aircraft Automated Collision Avoidance

Abstract
Aircraft collision avoidance is a pervasive need in this modern
age of flight. We present a 2-D automated collision avoidance flight
controller for automated collision avoidance amongst 2 aircraft.
This controller is designed to satisfy safety and liveness
requirements, implemented using Simulink and Stateflow, and
verified using safety and liveness monitors.
The Simulink & Stateflow model is available on GitHub here under an MIT License