KeYmaera 3.6.17

A powerful verification tool designed to be used by hybrid systems that include deductive, real algebraic, and computer algebraic technologies

KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems.

The application supports differential dynamic logic, which is a first-order dynamic logic for hybrid programs, a program notation for hybrid systems. It also supports hybrid systems with nonlinear discrete jumps, nonlinear differential equations, differential-algebraic equations, differential inequalities, and systems with nondeterministic discrete or continuous input.

For automation, KeYmaera implements a free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically.