一句话：提出异构动态逻辑 HDL，把不同动态逻辑视为可提升、可组合的动态理论，实现跨语言程序验证并提供机械化可靠性保证。
多编程语言系统的形式化验证通常需要组合不同程序逻辑，但现有方法难以模块化复用证明。本文提出异构动态逻辑 HDL，借鉴 SMT 的架构，将单个动态逻辑及其演算视为动态理论并进行组合。HDL 提供 lifting 与 combination 两种关键操作：lifting 为动态理论加入新程序构造并自动扩展可靠演算规则；combination 通过异构动态理论在单一模态下进行跨语言推理。作者用 regular programs 提升组合理论以获得异构控制结构，并在 Isabelle 中形式化动态理论、提升和组合，证明所有证明规则可靠。文章还给出结合动态逻辑与 Kleene Algebra with Tests 的规则，并证明提升与组合的相对完备性：在通常假设下，推理组合理论不比各组成理论及其公共一阶数据理论更难。最后用 Java 控制器与微分动态逻辑 plant 模型的汽车案例展示 HDL 的实用性。
Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL), a framework for combining reasoning principles from distinct (dynamic) program logics in a modular and compositional way. HDL mirrors the architecture of satisfiability modulo theories (SMT): Individual dynamic logics, along with their calculi, are treated as dynamic theories that can be combined to reason about heterogeneous systems whose components are verified using different program logics. HDL provides two key operations: Lifting extends an individual dynamic theory with new program constructs (e.g., the havoc operation or regular programs) and automatically augments its calculus with sound reasoning principles for the new constructs; and Combination enables cross-language reasoning in a single modality via Heterogeneous Dynamic Theories , facilitating the reuse of existing proof infrastructure. By lifting combined theories with regular programs, we obtain heterogeneous control structures that allow us to reason about intertwined cross-language behavior. We formalize dynamic theories, their lifting and combination, and prove the soundness of all proof rules in Isabelle. We also introduce a proof rule combining deductive DL-based reasoning with reasoning principles from Kleene Algebras with Tests. Furthermore, we prove relative completeness theorems for lifting and combination: Under usual assumptions, reasoning about lifted or combined theories is no harder than reasoning about the constituent dynamic theories and their common first-order structure (i.e., the data theory). We demonstrate HDL's value by verifying an automotive case study where a Java controller (formalized in Java dynamic logic) steers a plant model (formalized in differential dynamic logic).
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{TeuberUPB26,
title = {Heterogeneous Dynamic Logic: Provability Modulo Program Theories},
author = {Samuel Teuber and Mattias Ulbrich and André Platzer and Bernhard Beckert},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808295}
}