CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016
Tue 19 Jan 2016 10:30 - 11:00 at Room St Petersburg II - Session 6: Foundations

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 models of self-driving cars and collision avoidance protocols for aircraft. Unfortunately, these theorem provers do not have explicit proof terms, which makes the implementation of a number of important features unnecessarily complicated without soundness-critical and extra logical extensions to the theorem prover. Examples include: an unambiguous separation between proof checking and proof search, the ability to extract program traces corresponding to counter-examples, and synthesis of surely-live deterministic programs from liveness proofs for nondeterministic programs.

This paper presents a differential dynamic logic with such an explicit representation of proofs. The resulting logic extends both the syntax and semantics of differential dynamic logic with proof terms – syntactic representations of logical deductions. To support axiomatic theorem proving, the logic allows equivalence rewriting deep within formulas and supports both uniform renaming and uniform substitutions.

Tue 19 Jan

10:30 - 12:00: CPP - Session 6: Foundations at Room St Petersburg II
CPP-2016-main10:30 - 11:00
Nathan FultonCarnegie Mellon University, André Platzer
CPP-2016-main11:00 - 11:30
Floris van DoornCarnegie Mellon University
CPP-2016-main11:30 - 12:00
Vincent RahliSnT, Mark BickfordCornell University