KeYmaera is a free hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. KeYmaera is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems.
KeYmaera supports differential dynamic logic (dL) [12.] [10.] , which is a real-valued first-order dynamic logic for hybrid programs, a program notation for hybrid automata.
For automating the verification process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically.
Requirements:
· Java 1.5 or later
Find us on Google+
Universal Binary 
