pith. the verified trust layer for science. sign in

arxiv: 2507.08581 · v2 · submitted 2025-07-11 · 💻 cs.LO · cs.PL

Heterogeneous Dynamic Logic: Provability Modulo Program Theories

Samuel Teuber , Mattias Ulbrich , Andr\'e Platzer , Bernhard Beckert This is my paper

Pith reviewed 2026-05-19 05:38 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords Heterogeneous Dynamic LogicDynamic LogicModular VerificationProgram LogicsRelative CompletenessSoundness PreservationCross-Language ReasoningLifting and Combination
0
0 comments X p. Extension

The pith

Heterogeneous Dynamic Logic combines distinct program logics by lifting and combining them as dynamic theories while preserving soundness and relative completeness.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents Heterogeneous Dynamic Logic as a modular way to merge reasoning principles from separate dynamic program logics, treating each logic and its calculus as a reusable dynamic theory in the style of satisfiability modulo theories. Lifting adds new program constructs such as havoc or regular programs and automatically extends the existing calculus with sound rules for them. Combination then lets multiple such theories work together in one modality so that cross-language systems can be verified by reusing the original proof tools plus a shared first-order data theory. Relative completeness results show that the combined reasoning task remains no harder than the separate tasks plus the common data theory. The approach is demonstrated on a case study mixing a Java controller with a differential-equation plant model.

Core claim

Dynamic logics for different languages are treated as dynamic theories that support two operations: lifting, which extends a theory with new constructs and augments its calculus with sound rules, and combination, which produces heterogeneous dynamic theories for cross-language reasoning. Both operations are shown sound, and relative-completeness theorems establish that reasoning in the lifted or combined setting reduces to reasoning in the constituent logics together with their common first-order data theory. A further rule integrates deductive dynamic-logic reasoning with principles from Kleene algebras with tests, and all results are formalized in Isabelle.

What carries the argument

Lifting and combination operations on dynamic theories that automatically augment calculi while preserving soundness and relative completeness relative to the component logics and a shared data theory.

If this is right

  • All proof rules generated by lifting and combination remain sound.
  • Reasoning about a lifted or combined theory is no harder than reasoning separately in each constituent logic plus their common data theory.
  • Heterogeneous control structures obtained by lifting combined theories allow direct reasoning about intertwined cross-language execution.
  • Existing proof infrastructure for the separate logics can be reused without rebuilding a monolithic verifier.
  • A combined proof rule integrates standard dynamic-logic deduction with Kleene-algebra reasoning principles.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same lifting and combination steps could be iterated to handle systems that use three or more distinct program logics.
  • The framework naturally supports verification of embedded controllers where discrete software interacts with continuous physical models.
  • Applying the method to other language pairs, such as C and probabilistic programs, would test whether the relative-completeness guarantee scales beyond the Java-plus-differential-dynamics example.
  • The modular structure suggests a route to composing verification efforts across independently developed tool chains without requiring a single unified semantics.

Load-bearing premise

Each individual dynamic logic supplies a sound calculus that can be extended automatically when new constructs are added and that all logics share a common first-order data theory.

What would settle it

A concrete counter-example in which lifting a dynamic logic with a new construct produces an unsound rule that is accepted by the automatic augmentation procedure, or a combined theory for which relative completeness fails despite holding for each component.

Figures

Figures reproduced from arXiv: 2507.08581 by Andr\'e Platzer, Bernhard Beckert, Mattias Ulbrich, Samuel Teuber.

Figure 1
Figure 1. Figure 1: Elementary axioms and proof rules for dynamic theories [PITH_FULL_IMAGE:figures/full_fig_p011_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Axioms for Regular Programs Theorem 5.2 (Regular Closure over Dynamic Theory). For any dynamic theory Δ, its regular closure over programs Λ reg 𝑃 , P reg (see Definition 5.2) and FVreg 𝑃 as defined in Definition D.2 we get that Δ reg = Λ𝑉 , Λ𝐴, Λ reg 𝑃  , [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Results on Relative Completeness Proof. Using the notation from [PITH_FULL_IMAGE:figures/full_fig_p023_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Additional proof rules for Dynamic Theories. All rules pictured here are derivable from the axioms of [PITH_FULL_IMAGE:figures/full_fig_p032_4.png] view at source ↗
read the original abstract

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

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper introduces Heterogeneous Dynamic Logic (HDL) for modular combination of distinct dynamic program logics by treating them as dynamic theories. It defines lifting to extend theories with new constructs (e.g., havoc or regular programs) while automatically augmenting calculi with sound rules, and combination to enable cross-language reasoning in a single modality via Heterogeneous Dynamic Theories. All proof rules are shown sound in Isabelle; relative completeness theorems are proved under usual assumptions, stating that reasoning about lifted/combined theories is no harder than in the constituents plus their common first-order data theory. A new rule combining deductive DL reasoning with Kleene Algebras with Tests is introduced, and the framework is demonstrated on an automotive case study verifying a Java controller (in Java DL) steering a plant (in differential dynamic logic).

Significance. If the results hold, HDL provides a modular, SMT-like architecture for heterogeneous verification that reuses existing proof infrastructure across languages, which is a notable contribution for multi-language systems. The machine-checked Isabelle soundness proofs are a clear strength, lending high confidence to the core rules. The relative completeness results, if the data-theory assumption can be discharged in practice, would support the claim of tractable cross-language reasoning without disproportionate overhead.

major comments (1)
  1. [relative completeness theorems for lifting and combination] Relative completeness theorems for lifting and combination (as stated after the soundness results and in the abstract): the claim that reasoning is 'no harder than reasoning about the constituent dynamic theories and their common first-order structure' is load-bearing for the modularity benefit, yet the Java DL + dL case study involves distinct domains (object models versus real arithmetic) whose unification into a common data theory is not explicitly validated; without details on the encoding or additional proof obligations this unification imposes, the practical force of the 'no harder than' guarantee remains unclear.
minor comments (1)
  1. [automotive case study] The case study would benefit from a short table or paragraph explicitly listing the shared data-theory axioms used to bridge the Java object model and real arithmetic.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading of the manuscript and the constructive comments. The positive assessment of the modular architecture, the Isabelle soundness proofs, and the potential significance for multi-language verification is appreciated. We respond to the single major comment below.

read point-by-point responses

  1. Referee: [relative completeness theorems for lifting and combination] Relative completeness theorems for lifting and combination (as stated after the soundness results and in the abstract): the claim that reasoning is 'no harder than reasoning about the constituent dynamic theories and their common first-order structure' is load-bearing for the modularity benefit, yet the Java DL + dL case study involves distinct domains (object models versus real arithmetic) whose unification into a common data theory is not explicitly validated; without details on the encoding or additional proof obligations this unification imposes, the practical force of the 'no harder than' guarantee remains unclear.

    Authors: We agree that the practical force of the relative completeness results depends on the existence of a suitable common first-order data theory and that the case study would benefit from explicit discussion of this point. The theorems establish that, under the standard assumption of a shared data theory interpreting the relevant sorts and operations of both logics, reasoning in the lifted or combined theory reduces to reasoning in the constituents plus the data theory. For the Java DL + dL case study, the common data theory is the first-order theory of real arithmetic (capturing the continuous dynamics) extended with a sort for object references together with uninterpreted functions and predicates to abstract the discrete Java object state and method effects. This is a conventional encoding in hybrid verification settings. Nevertheless, the manuscript does not supply the concrete encoding details or discuss the resulting proof obligations. We will therefore revise the case-study section to include a short subsection that (i) defines the common data theory, (ii) sketches the embedding of the Java object model, and (iii) confirms that the additional obligations remain within the scope of the constituent theories. This clarification will be added without changing any theorems or proofs. revision: yes

Circularity Check

0 steps flagged

No significant circularity; results rest on explicit Isabelle proofs

full rationale

The paper defines dynamic theories, lifting, and combination operations, then proves soundness of all rules and relative completeness theorems directly in Isabelle. Relative completeness is conditional on external assumptions (sound calculi for base logics plus a common first-order data theory) rather than any quantity defined inside the HDL results themselves. No step reduces a claimed prediction or completeness result to a fitted parameter or self-referential definition by construction. Machine-checked proofs supply independent verification, and any self-citations to prior dL work are not load-bearing for the new HDL theorems.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The framework introduces new concepts grounded in standard assumptions of dynamic logic and first-order theories rather than ad-hoc fitted parameters.

axioms (2)
  • domain assumption Individual dynamic logics admit sound calculi that can be extended during lifting
    Invoked to guarantee that lifted and combined theories remain sound.
  • domain assumption Existence of a common first-order data theory shared by the combined logics
    Required for the relative completeness statement.
invented entities (1)
  • Heterogeneous Dynamic Theory no independent evidence
    purpose: Modular container for combined dynamic logics
    Newly defined construct enabling cross-language reasoning.

pith-pipeline@v0.9.0 · 5817 in / 1307 out tokens · 76903 ms · 2026-05-19T05:38:17.491895+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

  • IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean reality_from_one_distinction unclear
    ?
    unclear

    Relation between the paper passage and the cited Recognition theorem.

    HDL provides lifting and combination operations on dynamic theories that preserve soundness and achieve relative completeness, enabling modular cross-language verification no harder than reasoning in the constituent logics plus their common data theory.

  • IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear
    ?
    unclear

    Relation between the paper passage and the cited Recognition theorem.

    We also prove relative completeness theorems for lifting and combination: Under common 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”).

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

63 extracted references · 63 canonical work pages

  1. [1]

    Complete First-Order Game Logic

    Noah Abou El Wafa and André Platzer. “Complete First-Order Game Logic”. In: CoRR abs/2504.03495 (2025). doi: 10.48550/ARXIV.2504.03495

    work page doi:10.48550/arxiv.2504.03495 2025

  2. [2]

    Going Beyond Bell’s Theorem,

    Wolfgang Ahrendt et al., eds. Deductive Software Verification - The KeY Book - From Theory to Practice. Vol. 10001. LNCS. Cham: Springer, 2016. isbn: 978-3-319-49811-9. doi: 10.1007/978- 3-319-49812-6

    work page doi:10.1007/978- 2016

  3. [3]

    The Many Uses of Dynamic Logic

    Wolfgang Ahrendt et al. “The Many Uses of Dynamic Logic”. In: Go Where the Bugs Are: Essays Dedicated to Wolfgang Reif on the Occasion of His 65th Birthday . Ed. by Gidon Ernst et al. Cham: Springer Nature Switzerland, 2025, pp. 56–82. doi: 10.1007/978-3-031-92196-4_4

    work page doi:10.1007/978-3-031-92196-4_4 2025

  4. [4]

    Leveraging rust types for modular specification and verification

    Vytautas Astrauskas et al. “Leveraging rust types for modular specification and verification”. In: Proc. ACM Program. Lang. 3.OOPSLA (2019), 147:1–147:30. doi: 10.1145/3360573

    work page doi:10.1145/3360573 2019

  5. [5]

    Boogie: a modular reusable verifier for object-oriented programs

    Mike Barnett et al. “Boogie: a modular reusable verifier for object-oriented programs”. In: Proceedings of the 4th International Conference on Formal Methods for Components and Objects. FMCO’05. Amsterdam, The Netherlands: Springer-Verlag, 2005, pp. 364–387.isbn: 3540367497. doi: 10.1007/11804192_17. url: https://doi.org/10.1007/11804192_17

    work page doi:10.1007/11804192_17 2005

  6. [6]

    Satisfiability modulo theories

    Clark Barrett and Cesare Tinelli. “Satisfiability modulo theories”. In: Handbook of Model Checking. Ed. by Edmund M Clarke et al. Cham: Springer International Publishing, 2018, pp. 305–343. isbn: 978-3-319-10575-8. doi: 10.1007/978-3-319-10575-8_11

    work page doi:10.1007/978-3-319-10575-8_11 2018

  7. [7]

    A Dynamic Logic for the Formal Verification of Java Card Programs

    Bernhard Beckert. “A Dynamic Logic for the Formal Verification of Java Card Programs”. In: Java on Smart Cards: Programming and Security, First International Workshop, JavaCard 2000, Cannes, France, September 14, 2000, Revised Papers . Ed. by Isabelle Attali and Thomas P. Jensen. Vol. 2041. LNCS. Springer, 2000, pp. 6–24. doi: 10.1007/3-540-45165-X_2. Pre...

    work page doi:10.1007/3-540-45165-x_2 2000

  8. [8]

    Dynamic Logic with Non-rigid Functions: A Basis for Object-oriented Program Verification

    Bernhard Beckert and André Platzer. “Dynamic Logic with Non-rigid Functions: A Basis for Object-oriented Program Verification.” In:IJCAR. Ed. by Ulrich Furbach and Natarajan Shankar. Vol. 4130. LNCS. ISSN: 0302-9743. Springer, 2006, pp. 266–280. isbn: 3-540-37187-7. doi: 10.1007/11814771_23

    work page doi:10.1007/11814771_23 2006

  9. [10]

    Information Flow in Object-Oriented Software

    Bernhard Beckert et al. “Information Flow in Object-Oriented Software”. In: Logic-Based Program Synthesis and Transformation, 23rd International Symposium, LOPSTR 2013, Madrid, Spain, September 18-19, 2013, Revised Selected Papers . Ed. by Gopal Gupta and Ricardo Peña. Vol. 8901. LNCS. Cham: Springer, 2013, pp. 19–37. doi: 10.1007/978-3-319-14125-1_2

    work page doi:10.1007/978-3-319-14125-1_2 2013

  10. [11]

    The VerCors Tool for Verification of Concurrent Pro- grams

    Stefan Blom and Marieke Huisman. “The VerCors Tool for Verification of Concurrent Pro- grams”. In: FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16,

    work page 2014

  11. [12]

    Proceedings. Ed. by Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun. Vol. 8442. LNCS. Springer, 2014, pp. 127–131. doi: 10.1007/978-3-319-06410-9_9

    work page doi:10.1007/978-3-319-06410-9_9 2014

  12. [13]

    Formal Specification and Verification of JDK’s Identity Hash Map Implementation

    Martin de Boer et al. “Formal Specification and Verification of JDK’s Identity Hash Map Implementation”. In: Formal Aspects Comput. 35.3 (2023), 18:1–18:26. doi: 10.1145/3594729

    work page doi:10.1145/3594729 2023

  13. [14]

    Differential Dynamic Logic

    Rose Bohrer. “Differential Dynamic Logic”. In:Archive of Formal Proofs (Feb. 2017). https: //isa-afp.org/entries/Differential_Dynamic_Logic.html, Formal proof development. issn: 2150-914x

    work page 2017

  14. [15]

    A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow

    Rose Bohrer and André Platzer. “A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow”. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018 . Ed. by Anuj Dawar and Erich Grädel. ACM, 2018, pp. 115–124. doi: 10.1145/3209108.3209151

    work page doi:10.1145/3209108.3209151 2018

  15. [16]

    Verification modulo theories

    Alessandro Cimatti et al. “Verification modulo theories”. In:Formal Methods Syst. Des. 60.3 (2022), pp. 452–481. doi: 10.1007/S10703-023-00434-X

    work page doi:10.1007/s10703-023-00434-x 2022

  16. [17]

    A Tool for Checking ANSI-C Pro- grams

    Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. “A Tool for Checking ANSI-C Pro- grams”. In: Tools and Algorithms for the Construction and Analysis of Systems, 10th Inter- national Conference, TACAS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings . Ed. by Kurt Jensen and Andreas Podelski. Vol. 2988. LNCS. Springer, 2004, pp. 168–176. do...

    work page doi:10.1007/978-3-540-24730-2_15 2004

  17. [18]

    A new introduction to modal logic

    Maxwell John Cresswell and George Edward Hughes. A new introduction to modal logic . Routledge, 2012

    work page 2012

  18. [19]

    Guarded commands, nondeterminacy and formal derivation of pro- grams

    Edsger W. Dijkstra. “Guarded commands, nondeterminacy and formal derivation of pro- grams”. In: Commun. ACM 18.8 (Aug. 1975), pp. 453–457. issn: 0001-0782. doi: 10.1145/ 360933.360975. url: https://doi.org/10.1145/360933.360975

    work page doi:10.1145/360933.360975 1975

  19. [20]

    Why3 – Where Programs Meet Provers

    Jean-Christophe Filliâtre and Andrei Paskevich. “Why3 – Where Programs Meet Provers”. In: Proceedings of the 22nd European Symposium on Programming . Ed. by Matthias Felleisen and Philippa Gardner. Vol. 7792. LNCS. Springer, Mar. 2013, pp. 125–128

    work page 2013

  20. [21]

    Hybrid Relations in Isabelle/UTP

    Simon Foster. “Hybrid Relations in Isabelle/UTP”. In: Unifying Theories of Programming - 7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Porto, Portugal, October 8, 2019, Proceedings . Ed. by Pedro Ribeiro and Augusto Sampaio. Vol. 11885. LNCS. Springer, 2019, pp. 130–153. doi: 10.1007/978-3-030-31038-7_7

    work page doi:10.1007/978-3-030-31038-7_7 2019

  21. [22]

    Isabelle/UTP: A Mechanised Theory Engi- neering Framework

    Simon Foster, Frank Zeyda, and Jim Woodcock. “Isabelle/UTP: A Mechanised Theory Engi- neering Framework”. In: Unifying Theories of Programming - 5th International Symposium, Preprint 28 Samuel Teuber, Mattias Ulbrich, André Platzer, and Bernhard Beckert UTP 2014, Singapore, May 13, 2014, Revised Selected Papers. Ed. by David A. Naumann. Vol. 8963. LNCS. S...

    work page doi:10.1007/978-3-319-14806-9_2 2014

  22. [23]

    KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems

    Nathan Fulton et al. “KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems”. In: Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings . Ed. by Amy P. Felty and Aart Middeldorp. Vol. 9195. LNCS. Springer, 2015, pp. 527–538. doi: 10.1007/978-3-319-21401- 6_36

    work page doi:10.1007/978-3-319-21401- 2015

  23. [24]

    Fibring logics

    Dov M Gabbay. Fibring logics. Vol. 38. Clarendon Press, 1998

    work page 1998

  24. [25]

    An Overview of Fibred Semantics and the Combination of Logics

    Dov M. Gabbay. “An Overview of Fibred Semantics and the Combination of Logics”. In: Frontiers of Combining Systems: First International Workshop, Munich, March 1996 . Ed. by Frans Baader and Klaus U. Schulz. Dordrecht: Springer Netherlands, 1996, pp. 1–55. isbn: 978-94-009-0349-4. doi: 10.1007/978-94-009-0349-4_1. url: https://doi.org/10.1007/978-94- 009-0349-4_1

    work page doi:10.1007/978-94-009-0349-4_1 1996

  25. [26]

    HyPLC: hybrid programmable logic controller program translation for verification

    Luis Garcia, Stefan Mitsch, and André Platzer. “HyPLC: hybrid programmable logic controller program translation for verification”. In: Proceedings of the 10th ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2019, Montreal, QC, Canada, April 16-18, 2019 . Ed. by Xue Liu et al. ACM, 2019, pp. 47–56. doi: 10.1145/3302509.3311036

    work page doi:10.1145/3302509.3311036 2019

  26. [27]

    Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I

    Kurt Gödel. “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”. In: Monatshefte für mathematik und physik 38 (1931), pp. 173–198

    work page 1931

  27. [28]

    Verifying OpenJDK’s Sort Method for Generic Collections

    Stijn de Gouw et al. “Verifying OpenJDK’s Sort Method for Generic Collections”. In:J. Autom. Reason. 62.1 (2019), pp. 93–126. doi: 10.1007/S10817-017-9426-4

    work page doi:10.1007/s10817-017-9426-4 2019

  28. [29]

    First-Order Dynamic Logic

    David Harel. First-Order Dynamic Logic. Vol. 68. LNCS. Springer, 1979. isbn: 3-540-09237-4. doi: 10.1007/3-540-09237-4

    work page doi:10.1007/3-540-09237-4 1979

  29. [30]

    Dynamic Logic

    David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic Logic. The MIT Press, Sept. 2000. isbn: 978-0-262-27495-1. doi: 10.7551/mitpress/2516.001.0001. url: https://doi.org/10.7551/ mitpress/2516.001.0001

    work page doi:10.7551/mitpress/2516.001.0001 2000

  30. [31]

    An Axiomatic Basis for Computer Programming

    C. A. R. Hoare. “An Axiomatic Basis for Computer Programming”. In:Commun. ACM 12.10 (1969), pp. 576–580. doi: 10.1145/363235.363259

    work page doi:10.1145/363235.363259 1969

  31. [32]

    Unified theories of programming

    Charles Anthony Richard Hoare. “Unified theories of programming”. In: Mathematical methods in program development . Springer. 1997, pp. 313–367

    work page 1997

  32. [33]

    A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system

    Jean-Baptiste Jeannin et al. “A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system”. In: Int. J. Softw. Tools Technol. Transf. 19.6 (2017), pp. 717–741. doi: 10.1007/S10009-016-0434-1

    work page doi:10.1007/s10009-016-0434-1 2017

  33. [34]

    The MoXI Model Exchange Tool Suite

    Chris Johannsen et al. “The MoXI Model Exchange Tool Suite”. In:Computer Aided Verification - 36th International Conference, CA V 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I. Ed. by Arie Gurfinkel and Vijay Ganesh. Vol. 14681. LNCS. Springer, 2024, pp. 203–218. doi: 10.1007/978-3-031-65627-9_10

    work page doi:10.1007/978-3-031-65627-9_10 2024

  34. [35]

    Verified Train Controllers for the Federal Railroad Administration Train Kinematics Model: Balancing Competing Brake and Track Forces

    Aditi Kabra, Stefan Mitsch, and André Platzer. “Verified Train Controllers for the Federal Railroad Administration Train Kinematics Model: Balancing Competing Brake and Track Forces”. In: IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41.11 (2022), pp. 4409–4420. issn: 0278-0070. doi: 10.1109/TCAD.2022.3197690

    work page doi:10.1109/tcad.2022.3197690 2022

  35. [36]

    A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems

    Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle. “A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems”. In:Leibniz Trans. Embed. Syst. 8.2 (2022), 04:1–04:34. doi: 10.4230/LITES.8.2.4

    work page doi:10.4230/lites.8.2.4 2022

  36. [37]

    Frama-C: A software analysis perspective

    Florent Kirchner et al. “Frama-C: A software analysis perspective”. In:Formal Aspects Comput. 27.3 (2015), pp. 573–609. doi: 10.1007/S00165-014-0326-7. Preprint Heterogeneous Dynamic Logic: Provability Modulo Program Theories 29

    work page doi:10.1007/s00165-014-0326-7 2015

  37. [38]

    QIn: Enabling Formal Methods to Deal with Quantum Circuits

    Jonas Klamroth et al. “QIn: Enabling Formal Methods to Deal with Quantum Circuits”. In: IEEE International Conference on Quantum Software, QSW 2023, Chicago, IL, USA, July 2-8,

    work page 2023

  38. [39]

    by Shaukat Ali et al

    Ed. by Shaukat Ali et al. IEEE, 2023, pp. 175–185. doi: 10.1109/QSW59989.2023.00029

    work page doi:10.1109/qsw59989.2023.00029 2023

  39. [40]

    Verus: Verifying Rust Programs using Linear Ghost Types

    Andrea Lattuada et al. “Verus: Verifying Rust Programs using Linear Ghost Types”. In:Proc. ACM Program. Lang. 7.OOPSLA1 (2023), pp. 286–315. doi: 10.1145/3586037

    work page doi:10.1145/3586037 2023

  40. [41]

    Differential Refinement Logic

    Sarah M. Loos and André Platzer. “Differential Refinement Logic”. In:LICS. Ed. by Martin Grohe, Eric Koskinen, and Natarajan Shankar. ACM, 2016, pp. 505–514.doi: 10.1145/2933575. 2934555

    work page doi:10.1145/2933575 2016

  41. [42]

    Viper: A Verification Infras- tructure for Permission-Based Reasoning

    Peter Müller, Malte Schwerhoff, and Alexander J. Summers. “Viper: A Verification Infras- tructure for Permission-Based Reasoning”. In: Verification, Model Checking, and Abstract Interpretation, 17th Intl. Conf., VMCAI, St. Petersburg, FL, USA . Ed. by Barbara Jobstmann and K. Rustan M. Leino. Vol. 9583. LNCS. Springer, 2016, pp. 41–62

    work page 2016

  42. [43]

    Simplification by Cooperating Decision Procedures

    Greg Nelson and Derek C. Oppen. “Simplification by Cooperating Decision Procedures”. In: ACM Trans. Program. Lang. Syst. 1.2 (1979), pp. 245–257. doi: 10.1145/357073.357079

    work page doi:10.1145/357073.357079 1979

  43. [44]

    Relational Connectors and Heterogeneous Simulations

    Pedro Nora et al. “Relational Connectors and Heterogeneous Simulations”. In:Foundations of Software Science and Computation Structures - 28th International Conference, FoSSaCS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings . Ed. by Parosh Aziz Abdulla and Delia Kesner. Vol. 15691. LNCS. Springer, 2025, pp. 111–132. doi: 10.1007/978-3-031-90897-2\_6

    work page doi:10.1007/978-3-031-90897-2 2025

  44. [45]

    Complexity, Convexity and Combinations of Theories

    Derek C. Oppen. “Complexity, Convexity and Combinations of Theories”. In:Theor. Comput. Sci. 12 (1980), pp. 291–302. doi: 10.1016/0304-3975(80)90059-6

    work page doi:10.1016/0304-3975(80)90059-6 1980

  45. [46]

    Verifying Functional Correctness Properties at the Level of Java Bytecode

    Marco Paganoni and Carlo A. Furia. “Verifying Functional Correctness Properties at the Level of Java Bytecode”. In: Formal Methods - 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings . Ed. by Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker. Vol. 14000. LNCS. Springer, 2023, pp. 343–363. doi: 10.1007/978-3-031- 2...

    work page doi:10.1007/978-3-031- 2023

  46. [47]

    A Complete Uniform Substitution Calculus for Differential Dynamic Logic

    André Platzer. “A Complete Uniform Substitution Calculus for Differential Dynamic Logic”. In: J. Autom. Reason. 59.2 (2017), pp. 219–265. doi: 10.1007/s10817-016-9385-1

    work page doi:10.1007/s10817-016-9385-1 2017

  47. [48]

    Differential Dynamic Logic for Hybrid Systems

    André Platzer. “Differential Dynamic Logic for Hybrid Systems”. In:J. Autom. Reason. 41.2 (2008), pp. 143–189. doi: 10.1007/s10817-008-9103-8

    work page doi:10.1007/s10817-008-9103-8 2008

  48. [49]

    The complete proof theory of hybrid systems

    André Platzer. “The complete proof theory of hybrid systems”. In:Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012 . {IEEE} Computer Society, 2012, pp. 541–550. isbn: 978-0-7695-4769-5. doi: 10.1109/LICS.2012.64

    work page doi:10.1109/lics.2012.64 2012

  49. [50]

    European Train Control System: A Case Study in Formal Verification

    André Platzer and Jan-David Quesel. “European Train Control System: A Case Study in Formal Verification”. In:Formal Methods and Software Engineering, 11th International Confer- ence on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings. Ed. by Karin K. Breitman and Ana Cavalcanti. Vol. 5885. LNCS. Springer, 20...

    work page doi:10.1007/978-3-642-10373-5_13 2009

  50. [51]

    Differential Equation Invariance Axiomatization

    André Platzer and Yong Kiam Tan. “Differential Equation Invariance Axiomatization”. In:J. ACM 67.1 (2020), 6:1–6:66. doi: 10.1145/3380825

    work page doi:10.1145/3380825 2020

  51. [52]

    Uniform Substitution for Differential Refinement Logic

    Enguerrand Prebet and André Platzer. “Uniform Substitution for Differential Refinement Logic”. In: Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II . Ed. by Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt. Vol. 14740. LNCS. Springer, 2024, pp. 196–215. doi: 10.1007/9...

    work page doi:10.1007/978-3- 2024

  52. [53]

    Modelling and Verification of High- way Car Control with KeYmaera X

    Enguerrand Prebet, Samuel Teuber, and André Platzer. “Modelling and Verification of High- way Car Control with KeYmaera X”. In:Rigorous State-Based Methods - 11th International Conference, ABZ 2025, Düsseldorf, Germany, Proceedings . Ed. by Michael Leuschel and Fuyuki Ishikawa. Vol. 15728. LNCS. Springer, 2025. Preprint 30 Samuel Teuber, Mattias Ulbrich, ...

    work page 2025

  53. [54]

    Classes of recursively enumerable sets and their decision problems

    Henry Gordon Rice. “Classes of recursively enumerable sets and their decision problems”. In: Transactions of the American Mathematical society 74.2 (1953), pp. 358–366

    work page 1953

  54. [55]

    Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic

    Philipp Rümmer and Muhammad Ali Shah. “Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic”. In:Tests and Proofs - 1st International Conference, TAP 2007, Zurich, Switzerland, February 12-13, 2007. Revised Papers . Ed. by Yuri Gurevich and Bertrand Meyer. Vol. 4454. LNCS. Springer, 2007, pp. 41–60. doi: 10.1007/978-3-540-73770-4_3

    work page doi:10.1007/978-3-540-73770-4_3 2007

  55. [56]

    Reasoning about Abstract State Machines: The WAM Case Study

    Gerhard Schellhorn and Wolfgang Ahrendt. “Reasoning about Abstract State Machines: The WAM Case Study”. In:J. Univers. Comput. Sci. 3.4 (1997), pp. 377–413. doi: 10.3217/JUCS- 003-04-0377

    work page doi:10.3217/jucs- 1997

  56. [57]

    An algorithm for reasoning about equality

    Robert E. Shostak. “An algorithm for reasoning about equality”. In:Commun. ACM 21.7 (July 1978), pp. 583–585. issn: 0001-0782. doi: 10.1145/359545.359570

    work page doi:10.1145/359545.359570 1978

  57. [58]

    An axiomatic approach to existence and liveness for differential equations

    Yong Kiam Tan and André Platzer. “An axiomatic approach to existence and liveness for differential equations”. In:Formal Aspects Comput. 33.4-5 (2021), pp. 461–518. doi: 10.1007/ S00165-020-00525-0

    work page 2021

  58. [59]

    Provably Safe Neural Network Controllers via Differential Dynamic Logic

    Samuel Teuber, Stefan Mitsch, and André Platzer. “Provably Safe Neural Network Controllers via Differential Dynamic Logic”. In:Advances in Neural Information Processing Systems 38: Annual Conference on Neural Information Processing Systems 2024, NeurIPS 2024, Vancouver, BC, Canada, December 10 - 15, 2024 . Ed. by Amir Globersons et al. 2024

    work page 2024

  59. [60]

    A New Correctness Proof of the Nelson-Oppen Combination Procedure

    Cesare Tinelli and Mehdi T. Harandi. “A New Correctness Proof of the Nelson-Oppen Combination Procedure”. In: Frontiers of Combining Systems, First International Workshop FroCoS 1996, Munich, Germany, March 26-29, 1996, Proceedings . Ed. by Franz Baader and Klaus U. Schulz. Vol. 3. Applied Logic Series. Kluwer Academic Publishers, 1996, pp. 103–119. doi: ...

    work page doi:10.1007/978-94-009-0349-4_5 1996

  60. [61]

    Combining Decision Procedures for Sorted Theories

    Cesare Tinelli and Calogero G. Zarba. “Combining Decision Procedures for Sorted Theories”. In: Logics in Artificial Intelligence, 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27-30, 2004, Proceedings. Ed. by José Júlio Alferes and João Alexandre Leite. Vol. 3229. LNCS. Springer, 2004, pp. 641–653. doi: 10.1007/978-3-540-30227-8_53

    work page doi:10.1007/978-3-540-30227-8_53 2004

  61. [62]

    A Dynamic Logic for Unstructured Programs with Embedded Assertions

    Mattias Ulbrich. “A Dynamic Logic for Unstructured Programs with Embedded Assertions”. In: Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers . Ed. by Bernhard Beckert and Claude Marché. Vol. 6528. LNCS. Springer, 2010, pp. 168–182. doi: 10.1007/978-3-642-18070-5_12

    work page doi:10.1007/978-3-642-18070-5_12 2010

  62. [63]

    Dynamic logic for an intermediate language: verification, interaction and refinement

    Mattias Ulbrich. “Dynamic logic for an intermediate language: verification, interaction and refinement”. PhD thesis. Karlsruhe, Karlsruher Institut für Technologie (KIT), Diss., 2013, 2013

    work page 2013

  63. [64]

    Parameterized Dynamic Logic - Towards A Cyclic Logical Framework for Program Verification via Operational Semantics

    Yuanrui Zhang. Parameterized Dynamic Logic - Towards A Cyclic Logical Framework for Program Verification via Operational Semantics. 2024. doi: 10.48550/ARXIV.2404.18098. Preprint Heterogeneous Dynamic Logic: Provability Modulo Program Theories 31 A Additional Proof Rules A.1 Additional Proof Rules for Dynamic Theories Lemma A.1 (Helper Rules). The axioms ...

    work page doi:10.48550/arxiv.2404.18098 2024