André Platzer

A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics

2016

Differential dynamic logic is a logic for specifying and verifying safety, liveness, and other properties about models of cyber-physical systems. Theorem provers based on differential dynamic logic have been used to verify safety properties for …