Prof. Dr. Andre Platzer

Abstract:

Differential dynamic logic is a specification and verification logic for hybrid systems. It represents the theory behind the KeYmaera prover that has been used for verifying nontrivial properties of aircraft, railway, car control, and robotics applications.

This talk introduces a new relatively complete proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to use axioms instead of axiom schemata, substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of logical variables to restrict infinitely many axiom schema instances to sound ones, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms, which uniform substitutions instantiate soundly. The static semantics of differential dynamic logic and the soundness-critical restrictions it imposes on proof steps is captured exclusively in uniform substitutions and variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this article introduces differential forms for differential dynamic logic that make it possible to internalise differential invariants, differential substitutions, and derivations as first-class axioms to reason about differential equations. The resulting axiomatization of differential dynamic logic is proved to be sound and relatively complete.

This differential-form differential dynamic logic is the theory behind the new KeYmaera X theorem prover, an axiomatic tactical theorem prover for hybrid systems.