Verification project for hybrid systems in KeYmaera

Fall 2010

Chih-Yu Hsu
Andre Platzer
Project description

KeYmaera is an automated theorem prover serving as a verification tool for hybrid systems. By combining variable proof search strategies -- including deductive, differential equations, real arithmetic, etc -- and implementing a generalized sequent calculus, KeYmaera supports differential dynamic logic and verifies if the spec of hybrid systems guarantees its desired safety conditions. The objective of this project is to understand the general idea of verification workflow and get familiarized with KeYmaera by developing and solving verification problems starting from the magnetic field example. This project will investigate and solve new verification examples that have not been solved before - system concerning gravitational potential energy, kinetic energy, and elastic potential energy.

Return to project list