André Platzer

Programming and Proving with Dynamical Systems

Dynamic logic has been introduced for understanding programs, but its real calling are dynamical systems. Dynamic logic excels at providing simple and elegant logical foundations for the dynamical systems arising in cyber-physical systems. Since these CPSs combine cyber aspects such as communication and computer control with physical aspects such as movement in space, their dynamical system models also combine discrete dynamics with continuous dynamics. Differential dynamic logic provides a programming language for these models and comes with a compositional axiomatization and strong completeness guarantees. Its implementation in the KeYmaera X theorem prover has been instrumental in verifying applications such as the Airborne Collision Avoidance System ACAS X and ground robot navigation.

Some references