Heterogeneous Dynamic Logic: Provability Modulo Program Theories
summary
Heterogeneous Dynamic Logic treats each program logic as a dynamic theory and gives two concrete operations: Lifting to add constructs (havoc, regular programs) with reusable reduction rules, and Combination to form cross-language regular programs with heterogeneous reduction and a frame‑style rule. All proof rules and soundness are formalized in Isabelle, and relative‑completeness theorems show lifting/combination do not increase proof difficulty; an automotive Java+plant case study verifies the end‑to‑end controller and is available as reusable artifacts.
AI-written summary · about
chapters (10)
- 0:00Heterogeneous systems verification
- 1:26Motivation for program logics
- 3:09Heterogeneous dynamic logic
- 4:54Dynamic theories and semantics
- 8:03Calculus rules for dynamic theories
- 9:47Extending dynamic theories
- 12:37Combining dynamic theories
- 15:27Completeness and case study
- 16:31Conclusion and future work
- 16:52Q&A
related talks
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
01h 34mFormal Logic Undressed
29mA Temporal Differential Dynamic Logic Formal Embedding
19mExtensible Metatheory Mechanization via Family Polymorphism
15mTowards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
49mCompile-time Logic Programming in Scala: what for?
05mNew foundations for probabilistic separation logic
41mLiving inside a Theorem Proving Universe