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).

翻译：形式化地规约（更不用说验证）涉及多编程语言的系统特性本身就极具挑战性。我们提出异构动态逻辑（HDL），这是一种以模块化、组合化方式融合不同（动态）程序逻辑推理原则的框架。HDL 模仿了可满足性模理论（SMT）的架构：单个动态逻辑及其演算被视为动态理论，这些理论可以组合起来，用于推理那些其组件使用不同程序逻辑验证的异构系统。HDL 提供两种关键操作：提升操作通过新增程序构造（例如，破坏性赋值操作或正则程序）扩展单个动态理论，并自动为其演算补充针对新构造的可靠推理原则；组合操作则通过异构动态理论实现单一模态下的跨语言推理，从而促进现有证明基础设施的重用。通过使用正则程序提升组合后的理论，我们获得了异构控制结构，这使得我们能够推理交织的跨语言行为。我们在 Isabelle 中形式化了动态理论、它们的提升与组合，并证明了所有证明规则的可靠性。我们还引入了一条将基于演绎的 DL 推理与带测试的 Kleene 代数的推理原则相结合的证明规则。此外，我们证明了提升和组合的相对完备性定理：在通常的假设下，对提升或组合理论进行推理的难度，不会超过对组成它的动态理论及其共同的一阶结构（即数据理论）进行推理的难度。我们通过验证一个汽车领域的案例研究来展示 HDL 的价值：在该案例中，一个用 Java 动态逻辑形式化的 Java 控制器控制一个用微分动态逻辑形式化的受控对象模型。