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
Times are displayed in time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey change

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