A Temporal Differential Dynamic Logic Formal Embedding
summary
This work embeds dTL2 embedded in PVS by formalizing a trace semantics, a proof calculus extended for universally quantified reachability, and tactics so proofs can run interactively inside PVS rather than outsourcing ODE solving. The library extends the prior Platypus DL work, excludes error traces from semantics (which forces bidirectional rule schemas), supports abstract ODEs like X' = f(x) with property-based reasoning, and is fully functional for verifying hybrid programs with PVS commands and specialized strategies.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:04Research presentation
- 2:36PVS and formal embedding
- 5:11Hybrid systems formalization
- 8:46Differential Dynamic Logic semantics
- 13:11Temporal operators and traces
- 15:00Reasoning about intermediate states
- 17:51Eliminating error traces
- 20:02Comparison with provers
- 21:49Questions and discussion session
related talks
19mHeterogeneous Dynamic Logic: Provability Modulo Program Theories
57mStructural Embeddings Revisited
41mLiving inside a Theorem Proving Universe
20mMRPHS: Enabling Transaction-level Deductive Formal Verification Through PDVL
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
01h 07mBack to the Future: A Fresh Look at Linear Temporal Logic
01h 02mTheory and Control
01h 34mFormal Logic Undressed