Pith. sign in

REVIEW 3 major objections 5 minor 82 references

Toward Structured Proofs for Dynamic Logics

T0 review · 3 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Named past states simplify hybrid-system proofs without sacrificing completeness.

desk verdict Kaisar's nominal terms and structured symbolic execution are a genuine contribution to CPS proof engineering, but the completeness theorem rests on a sketched ODE normalization lemma that needs a real proof before the central claim is settled. read the letter →

arxiv 1908.05535 v1 pith:ZSG453PY submitted 2019-08-15 cs.PL cs.LO

Rose Bohrer , André Platzer This is my paper · ORCID
classification cs.PLcs.LO MSC 03B7068Q6068V15
keywords differentialdynamiclogicstructuredproofnominaltermshistoricalreferencesymbolicexecutioncyber-physicalsystemsinvariantsinteractivetheoremproving
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Kaisar is a structured interactive proof language for differential dynamic logic, the logic used to verify safety of cyber-physical systems that combine discrete programs with ordinary differential equations. The paper's central claim is that proof authors should be able to name past program states and write $t(\theta)$ for the value of term $\theta$ in the named state $t$, turning the historical reference that pervades hybrid-system proofs into a first-class language feature instead of manual ghost-state bookkeeping. It supports this with a metatheory showing Kaisar is sound and complete with respect to the standard dL sequent calculus, and that each nominal term really denotes the value of $\theta$ in the corresponding program state, including intermediate states. If correct, Kaisar removes a major source of proof clutter from cyber-physical-system verification while keeping the full expressiveness of dL.

What carries the argument

The load-bearing mechanism is structured symbolic execution backed by static execution traces and nominal terms. A static trace is an ordered list of trace records—$sub(x,\theta)$, $eq(x,x_i,\theta)$, $any(x,x_i)$, and state markers $t$—maintained automatically by Kaisar's proof rules; the sequent-level state is defined from the corresponding dynamic trace, so each variable's current name can be computed by replaying the trace. The nominal term $t(\theta)$ works by resolving each variable to the name it had at named state $t$, then translating that name through the trace to the present proof state. This single device carries the paper's automation: it is what makes historical references first-class, what the soundness and completeness theorems are about, and what relates Kaisar to the nominal logic dLh.

What would settle it

Instrument the implementation to log, for every nominal term $t(\theta)$ in the parachute and ground-robot proofs, the ghost substitution that resolves it, and compare that value with the term's value in the recorded program state at state $t$; any mismatch would refute Theorem 7.6. Alternatively, construct a dL-derivable ODE sequent whose sequent-calculus proof cannot be rearranged into the linear-normal form of Lemma 7.16, which would refute the completeness theorem.

Watch

Extended reading notes

Core claim

At the center of the paper is the observation that every dL proof step that changes a program state can be recorded in a static execution trace: substitution records, ghost-variable equality records, arbitrary-assignment records, and named-state markers. Given such a trace, a nominal term $t(\theta)$ is resolved by replaying the trace to find which name each variable has at state $t$ and then translating that name back to the current sequent-level state. The paper proves this resolution correct in Theorem 7.6 (Nominal Term Correspondence), shows the correspondence persists inside every proof state in Theorem 7.7, and establishes in Theorems 7.14 and 7.15 that the resulting proof language is sound and complete for dL. Completeness for continuous dynamics is obtained by Lemma 7.16, which asserts that any ODE proof in the dL sequent calculus can be normalized to a linear-normal form—differential ghosts, then differential-invariant cuts, then differential weakening—so that Kaisar's invariant, ghost, and solve rules cover all ODE reasoning. The nominalization theorem also connects Kaisar's named states to the nominal hybrid logic dLh, giving a logic-level specification of what the names mean.

Load-bearing premise

The completeness result for differential equations rests on a lemma, proved only by sketch in the paper, that every ODE proof in the dL sequent calculus can be rearranged into one fixed normal form; if that lemma fails, Kaisar's completeness for continuous dynamics fails too.

Editorial extensions

If this is right

  • Hybrid-system proofs can refer explicitly to initial, intermediate, and loop-entry states without the author manually introducing ghost variables; the structured symbolic execution supplies the needed ghost state automatically.
  • Kaisar is complete with respect to the dL sequent calculus, so the convenience of nominals costs no provability: every dL theorem remains provable in Kaisar.
  • Nominal terms are governed by a correspondence theorem, so a proof text that writes $t(\theta)$ is a faithful description of the program's actual behavior at the named state.
  • The same mechanism covers both discrete programs and ordinary differential equations, including equations without closed-form solutions, via the solve, differential-invariant, and differential-ghost rules.
  • The implementation reproduces a parachute-safety proof and a ground-robot case study, indicating the language scales to realistic verification problems.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The record-replay design is not specific to dL: any program logic whose proof rules introduce ghost variables or substitution bookkeeping could adopt the same static-trace semantics, so the approach should port to separation logics and other Hoare-style logics.
  • Because ODE completeness rests on a sketched normalization lemma, a fully formalized proof of Lemma 7.16—or a concrete counterexample—would settle exactly how far Kaisar's continuous-dynamics completeness extends.
  • A direct empirical check of the core theorem is possible: instrument the implementation to log the ghost substitution produced for every nominal and compare it with the recorded program state in the two published examples; any mismatch would refute Theorem 7.6.
  • States named inside nondeterministic branches are deliberately local to that branch in the trace semantics; a natural extension would be a notion of branching or partial traces that lets nominals refer to branch-local states outside their scope.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper introduces Kaisar, a structured interactive proof language for differential dynamic logic (dL), whose defining feature is nominal terms that make historical references to past program states first-class. Kaisar extends structured proof with structured symbolic execution, and the paper presents its syntax, proof-checking rules, examples (a parachute safety proof and a ground-robot case study), and an implementation in KeYmaera X. The metatheory claims that Kaisar's nominal terms correctly denote values in historical program states (Theorem 7.6), that Kaisar is sound with respect to dL semantics (Theorem 7.14), and that Kaisar is complete with respect to the dL sequent calculus (Theorem 7.15), including a reduction of ODE reasoning to a linear-normal form (Lemma 7.16).

Significance. If the metatheory is completed and corrected, this is a valuable contribution: it gives the first structured proof language for dL with a principled treatment of historical state reference, provides a formal semantics for nominals via execution traces, and establishes relative completeness without restricting the expressiveness of dL. The implementation reuses the LCF-style sound core of KeYmaera X, whose soundness was mechanized in prior work, giving independent support for the implementation's trustworthiness. The nominal-term correspondence theorems and the proof-language connection to nominal dL (dLh) are conceptually novel and likely to influence future proof-language design for hybrid systems. However, as submitted, the central soundness and completeness theorems are not fully proven in the text: several load-bearing cases are explicitly omitted or only sketched, so the published-style proof is incomplete.

major comments (3)
  1. [§7.2, Lemma 7.16] The proof of Lemma 7.16, which claims that every ODE proof in the dL sequent calculus can be normalized to linear-normal form (DGs, DIs/DCs, DW), is only a sketch. In the DI case, the rewrite replaces a differential-induction step with a differential cut whose first premise is the very formula proved by that DI; the sketch does not explain how the two DC premises are placed in the derivation tree without circularity, nor does it show that the rewritten derivation is well-founded. In the DC case, the proof concatenates the normal forms of the two cut premises, but the second premise lives in the strengthened domain Q∧C, and the assertion that cuts and ghosts 'do not reduce provability' is exactly the nontrivial content of the lemma; no proof of this assertion is supplied. Since Theorem 7.15's ODE cases and Lemma 7.17 rely directly on this normal form, the completeness half of the central claim is not fully established.
  2. [§7.2, Theorem 7.14] The proof of soundness (Theorem 7.14) explicitly states that the diamond rules and the implicit rules are left out, with the comment that they are 'analogous to the box rules' or 'follow directly from soundness of propositional logic and a handful of dL axioms.' The diamond rules in Appendix C are not fully symmetric to the box rules: for example, the diamond assignment rule (⟨:=⟩sub) has an admissibility condition, the diamond loop rule (⟨∗⟩) has a different structure, and the diamond ODE rule (⟨′⟩) generates an extra domain proof obligation. The soundness of these rules is part of the claim of Theorem 7.14, and 'analogous' is not a proof in a journal presentation. The omitted cases need to be supplied, or a rigorous reduction to the presented cases needs to be given.
  3. [§7.2, Theorem 7.15] The completeness proof (Theorem 7.15) says it presents only right rules for boxes and left rules for diamonds, with the other cases described as analogous. This is load-bearing because the lexicographic induction measure is claimed to strictly decrease in all cases, and the left-rule box cases are precisely where rule (1) of the measure (number of antecedent modalities) is supposed to apply; the well-foundedness of those cases is not demonstrated. In addition, Observation 1 requires that every state be named to make expansion surjective, and the proof does not show that this invariant is maintained in the omitted cases. As written, completeness for full dL sequent calculus is therefore not established.
minor comments (5)
  1. [§4, Focus paragraph] There is a typo: 'Hewever' should be 'However'.
  2. [Definition 5.2] The displayed definition of ωα appears malformed: 'ωα = η,ωω(y1) x1 ··· ω(xn)) yn' has unbalanced parentheses and unclear superscript/subscript placement; it should be rewritten.
  3. [Example 3, Figure 3] The line 'assumevEps >vBound_∧ r = ar' contains a stray final 'r'; it should presumably be 'r = a'.
  4. [Theorem 7.9 proof] The notation 'η,ω,ω∗ν' is not defined; it should likely read 'η,ω,η∗ν' or a definition of the trace concatenation should be given.
  5. [§7.2, soundness proof] In the case for loops in the soundness proof, the text refers to 'Lemma ??' without a number; this unresolved reference needs to be fixed.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: Kaisar's metatheory is an independent embedding into dL semantics; only Lemma 7.16's normalization sketch is a proof gap, not a circular step.

full rationale

I walked the claimed derivation chain. Kaisar's proof rules are defined with their own syntax and trace semantics; soundness (Theorem 7.14) is proved by induction on the Kaisar proof rules against the external dL denotational semantics, and completeness (Theorem 7.15) is shown by translating dL sequent-calculus proofs into Kaisar proofs under an explicit well-founded metric. Nominal-term correspondence (Theorems 7.6 and 7.7) is a consistency theorem for the trace semantics, not a quantity fitted from data and then renamed as a prediction. No parameters are fitted to subsets of examples, and no empirical benchmark is definitionally reused as the theorem being proved. The implementation reuses the LCF-style core of KeYmaera X from prior work [8, 23], which is independent, machine-checked support for the soundness of the underlying prover, rather than a self-citation that supplies the paper's central claims. Citations to prior work by the same authors, such as dLh [59], differential ghosts [62], and the implementability of the ODE solve axiom using DG/DC/DI [65], are used as external published theorems with stated assumptions; they do not assume the Kaisar results that the paper proves. The one substantive weakness is Section 7.2, Lemma 7.16: the claim that every ODE proof can be put into linear-normal form is justified only by a sketch, and the sketch relies on nontrivial admissibility properties such as "addition of further invariants ... does not reduce provability." If that normalization were false, the ODE half of Theorem 7.15 would fail. This is a correctness gap in a published-style proof, not a circular reduction: the lemma's conclusion is not identical by construction to any input of Kaisar or to any prior self-citation. The central derivation is therefore self-contained against the external dL standard, and no circularity score above 0 is warranted.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

No free parameters are fitted; the central contribution is a proof language with a semantic justification. The paper's claims rest on the established soundness and relative completeness of dL, the existence and uniqueness of ODE solutions in the dL semantics, and the soundness of KeYmaera X's LCF core from prior work.

assumptions (3)
  • standard math The dL sequent calculus is sound and relatively complete, used as the external standard for Kaisar's soundness and completeness.
    Invoked in Sections 7.2 and 7.3 to define the target of completeness and to justify soundness of the underlying logic.
  • domain assumption Hybrid programs' ODEs have unique solutions on their evolution domains, as required by dL denotational semantics.
    The semantics of ODE evolution is defined as the unique solution in Appendix B; this also underlies differential ghosts, whose soundness requires the ghost ODE to preserve the existence interval.
  • standard math The LCF-style core of KeYmaera X is sound, used to justify the soundness of the auto proof method.
    Footnote 1 and Section 8 rely on the mechanized soundness of KeYmaera X's core from prior work by Bohrer et al. 2017.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Toward Structured Proofs for Dynamic Logics." pith.science (2026). https://pith.science/paper/ZSG453PY

@misc{pith2026190805535,
  author       = {Pith},
  title        = {Pith review of: Toward Structured Proofs for Dynamic Logics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ZSG453PY}},
  note         = {Machine review of arXiv:1908.05535}
}
read the original abstract

We present Kaisar, a structured interactive proof language for differential dynamic logic (dL), for safety-critical cyber-physical systems (CPS). The defining feature of Kaisar is *nominal terms*, which simplify CPS proofs by making the frequently needed historical references to past program states first-class. To support nominals, we extend the notion of structured proof with a first-class notion of *structured symbolic execution* of CPS models. We implement Kaisar in the theorem prover KeYmaera X and reproduce an example on the safe operation of a parachute and a case study on ground robot control. We show how nominals simplify common CPS reasoning tasks when combined with other features of structured proof. We develop an extensive metatheory for Kaisar. In addition to soundness and completeness, we show a formal specification for Kaisar's nominals and relate Kaisar to a nominal variant of dL.

Figures

Figures reproduced from arXiv: 1908.05535 by the authors.

Figure 1
Figure 1. Kaisar Proofs of First-Order Example [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Kaisar Proofs of Skydiver Discrete Fragment [PITH_FULL_IMAGE:figures/full_fig_p013_2.png] view at source ↗
Figure 3
Figure 3. Kaisar Proof of Skydiver Safety Unlike in loops, it is essential for soundness that we do not assume the current invariant (only previous invariants) while proving it. Differential invariant [58] reasoning uses the differential of a formula (ϕ) ′ to compute its Lie derivative, and then proves it to be inductive. Traces are general enough to support loops and differental equations uniformly. Because the differential … view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Kaisar Proof of Bouncing Ball Safety 7 METATHEORY The value of a nominal t(θ) in the sequent-level state agrees with the value of θ in the corresponding program state. We begin here with the simplest case, pseudo-nominals of variables nowH (x), from which we then deriv…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

82 extracted references · 50 canonical work pages

  1. [1]

    Schmitt, and Mattias Ulbrich

    Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich. 2016. Deductive Software Verification - The KeY Book . Springer

    2016

  2. [2]

    Krzysztof Apt, Frank S De Boer, and Ernst-Rüdiger Olderog. 2010. Verification of sequential and concurrent programs. (2010)

    2010

  3. [3]

    Apt, Jan A

    Krzysztof R. Apt, Jan A. Bergstra, and Lambert G. L. T. Meertens. 1979. Recursive Assertions are not enough - or are they? Theor. Comput. Sci. 8 (1979), 73–87. https://doi.org/10.1016/0304-3975(79)90058-6

    work page doi:10.1016/0304-3975(79)90058-6 1979

  4. [4]

    Arnon, George E

    Dennis S. Arnon, George E. Collins, and Scott McCallum. 1984. Cylindrical Algebraic Decomposition I: The Basic Algorithm. SIAM J. Comput. 13, 4 (Nov. 1984), 865–877. https://doi.org/10.1137/0213054

    doi:10.1137/0213054 1984

  5. [5]

    Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, and Josef Urban. 2015. Mizar: State-of-the-art and Beyond.. In CICM (Lecture Notes in Computer Science) , Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge (Eds.), Vol. 9150. Springer, 261–279. https://doi.or...

    doi:10.1007/978-3-319-20615-8 2015

  6. [6]

    Mike Barnett, K Rustan M Leino, and Wolfram Schulte. 2005. The Spec{#} Programming System: An Overview . Springer Berlin Heidelberg, Berlin, Heidelberg, 49–69. https://doi.org/10.1007/978-3-540-30569-9_3

    work page doi:10.1007/978-3-540-30569-9_3 2005

  7. [7]

    Bruno Barras and Benjamin Werner. 1997. Coq in Coq. Technical Report. INRIA Rocquencourt

    work page 1997

  8. [8]

    Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer. 2017. Formally Verified Differential Dynamic Logic. In Certified Programs and Proofs - 6th ACM SIGPLAN Conference, CPP 2017, Paris, France, January 16-17, 2017, Yves Bertot and Viktor Vafeiadis (Eds.). ACM, 208–221

    work page 2017

Show all 82 references
  1. [9]

    Henzinger, and Arjun Radhakrishna

    Udi Boker, Thomas A. Henzinger, and Arjun Radhakrishna. 2014. Battery transition systems. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, Suresh Jagannathan and Peter Sewell (Eds.). ACM,...

    2014

  2. [10]

    Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. 2013. Flow*: An Analyzer for Non-linear Hybrid Systems . Springer Berlin Heidelberg, Berlin, Heidelberg, 258–263. https://doi.org/10.1007/978-3-642-39799-8_18

    2013 doi

  3. [11]

    Edmund M. Clarke. 1980. Proving Correctness of Coroutines Without History Variables. Acta Inf. 13 (1980), 169–188. https://doi.org/10.1007/BF00263992

    1980 doi

  4. [12]

    Maurice Clint. 1973. Program Proving: Coroutines. Acta Inf. 2 (1973), 50–63. https://doi.org/10.1007/BF00571463

    1973 doi

  5. [13]

    Collins and Hoon Hong

    George E. Collins and Hoon Hong. 1991. Partial Cylindrical Algebraic Decomposition for Quantifier Elimination. J. Symb. Comput. 12, 3 (Sept. 1991), 299–328. https://doi.org/10.1016/S0747-7171(08)80152-6

    1991 doi

  6. [14]

    Pierre Corbineau. 2007. A Declarative Language for the Coq Proof Assistant. In Types for Proofs and Programs, International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers (Lecture Notes in Computer Science) , Marino Miculan, Ivan Sca...

    2007 doi

  7. [15]

    Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. 2012. TLA + Proofs. In FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings (Lecture Notes in Computer Science) , Dimitra Gian...

    2012 doi

  8. [16]

    Davenport and Joos Heintz

    James H. Davenport and Joos Heintz. 1988. Real quantifier elimination is doubly exponential. Journal of Symbolic Computation 5, 1-2 (1988), 29–35. https://doi.org/10.1016/S0747-7171(88)80004-X

    1988 doi

  9. [17]

    Martin Davis. 1981. Obvious Logical Inferences. In Proceedings of the 7th International Joint Conference on Artificial Intelligence, IJCAI ’81, Vancouver, BC, Canada, August 24-28, 1981 , Patrick J. Hayes (Ed.). William Kaufmann, 530–531. http://ijcai.org/Proceedings/81-1/Pape...

    1981

  10. [18]

    David Delahaye. 2000. A Tactic Language for the System Coq. In Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (LPAR’00) . Springer-Verlag, Berlin, Heidelberg, 85–95. http: //dl.acm.org/citation.cfm?id=1765236.1765246

    2000

  11. [19]

    Tommaso Dreossi. 2017. Sapo: Reachability Computation and Parameter Synthesis of Polynomial Dynamical Systems. In Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, Pittsburgh, PA, USA, April 18-20, 2017, Goran Frehse and Sa...

    2017

  12. [20]

    Goran Frehse. 2005. PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. InHybrid Systems: Computation and Control, 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005, Proceedings (Lecture Notes in Computer Science), Manfred Morari and Loth...

    2005

  13. [21]

    Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable Verification of Hybrid Systems. In Computer Aided Verification - 23rd International Conference, CA ...

    2011 doi

  14. [22]

    Nathan Fulton, Stefan Mitsch, Brandon Bohrer, and André Platzer. 2017. Bellerophon: Tactical Theorem Proving for Hybrid Systems. In Interactive Theorem Proving - Eighth International Conference, ITP 2017, Brasilia, Brasil, September 26-29, 2017. To Appear. https://nfulton.org/...

    2017

  15. [23]

    Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and André Platzer. 2015. KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. In CADE (LNCS), Amy P. Felty and Aart Middeldorp (Eds.), Vol. 9195. Springer, 527–538. https://doi.org/10.1007/978-3-319-2...

    2015 doi

  16. [24]

    Sicun Gao, Soonho Kong, and Edmund M. Clarke. 2013. dReal: An SMT Solver for Nonlinear Theories over the Reals. In Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings (Lecture Notes in Compute...

    2013 doi

  17. [25]

    Sicun Gao, Soonho Kong, and Edmund M. Clarke. 2013. Satisfiability modulo ODEs. In Formal Methods in Computer- Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013 . IEEE, 105–112. http://ieeexplore.ieee.org/document/ 6679398/

    2013

  18. [26]

    Georges Gonthier and Assia Mahboubi. 2010. An introduction to small scale reflection in Coq. J. Formalized Reasoning 3, 2 (2010), 95–152. https://doi.org/10.6092/issn.1972-5787/1979

    2010 doi

  19. [27]

    Georges Gonthier and Enrico Tassi. 2012. A Language of Patterns for Subterm Selection. In Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings (Lecture Notes in Computer Science), Lennart Beringer and Amy P...

    2012

  20. [28]

    David Harel, Jerzy Tiuryn, and Dexter Kozen. 2000. Dynamic Logic. MIT Press, Cambridge, MA, USA

    2000

  21. [29]

    John Harrison. 1996. A Mizar Mode for HOL. In Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs’96, Turku, Finland, August 26-30, 1996, Proceedings (Lecture Notes in Computer Science) , Joakim von Wright, Jim Grundy, and John Harrison (Eds.), Vol. 11...

    1996 doi

  22. [30]

    Henzinger

    Thomas A. Henzinger. 1996. The Theory of Hybrid Automata. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996 . IEEE Computer Society, 278–292. https://doi.org/10.1109/LICS.1996.561342

    1996

  23. [31]

    Henzinger, Pei-Hsin Ho, and Howard Wong-Toi

    Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. 1997. HYTECH: A Model Checker for Hybrid Systems. In Computer Aided Verification, 9th International Conference, CA V ’97, Haifa, Israel, June 22-25, 1997, Proceedings (Lecture Notes in Computer Science), Orna Grumberg (Ed....

    1997 doi

  24. [32]

    C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (Oct. 1969), 576–580. https://doi.org/10.1145/363235.363259

    1969

  25. [33]

    Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, and André Platzer. 2015. Formal Verification of ACAS X, an Industrial Airborne Collision Avoidance System. In EMSOFT, Alain Girault and Nan Guan (Eds.). IEEE Press, 127–136. h...

    2015

  26. [34]

    Cezary Kaliszyk, Karol Pak, and Josef Urban. 2016. Towards a mizar environment for isabelle: foundations and language. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016, Jeremy Avigad and Adam Chli...

    2016

  27. [35]

    Kengo Kido, Swarat Chaudhuri, and Ichiro Hasuo. 2016. Abstract Interpretation with Infinitesimals - Towards Scalability in Nonstandard Static Analysis. In Verification, Model Checking, and Abstract Interpretation - 17th International Confer- ence, VMCAI 2016, St. Petersburg, F...

    2016 doi

  28. [36]

    Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2010. seL4: formal verification of an operating-system kernel. Commun. ...

    2010 doi

  29. [38]

    Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and...

    2017 doi

  30. [39]

    Leslie Lamport. 1992. Hybrid Systems in TLA +. In Hybrid Systems (Lecture Notes in Computer Science) , Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel (Eds.), Vol. 736. Springer, 77–102. https://doi.org/10.1007/ 3-540-57318-6_25

    1992

  31. [40]

    Leslie Lamport. 1995. How to Write a Proof. Amer. Math. Monthly 102, 7 (1995), 600–608. http://lamport.azurewebsites. net/pubs/lamport-how-to-write.pdf

    1995

  32. [41]

    Leslie Lamport. 2012. How to Write a 21st Century Proof. Journal of Fixed Point Theory and Applications (2012). https://doi.org/10.1007/s11784-012-0071-6

    2012 doi

  33. [42]

    Leavens, Albert L

    Gary T. Leavens, Albert L. Baker, and Clyde Ruby. 1999. JML: A Notation for Detailed Design. InBehavioral Specifications of Businesses and Systems , Haim Kilov, Bernhard Rumpe, and Ian Simmonds (Eds.). The Kluwer International Series in Engineering and Computer Science, Vol. 5...

    1999 doi

  34. [43]

    Rustan M

    K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. InLogic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers (Lecture Notes in ...

    2010 doi

  35. [44]

    Rustan M

    K. Rustan M. Leino, Peter Müller, and Jan Smans. 2009. Verification of Concurrent Programs with Chalice. In Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures (Lecture Notes in Computer Science), Alessandro Aldini, Gilles Barthe, and Roberto ...

    2009

  36. [45]

    Rustan Leino. 2008. This is Boogie 2. Microsoft Research. https://www.microsoft.com/en-us/research/publication/ this-is-boogie-2-2/

    2008

  37. [46]

    Andreas Lochbihler. 2007. Jinja with Threads. Archive of Formal Proofs 2007 (2007). https://www.isa-afp.org/entries/ JinjaThreads.shtml

    2007

  38. [47]

    Loos, André Platzer, and Ligia Nistor

    Sarah M. Loos, André Platzer, and Ligia Nistor. 2011. Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified. In FM (LNCS) , Michael Butler and Wolfram Schulte (Eds.), Vol. 6664. Springer, 42–56. https: //doi.org/10.1007/978-3-642-21437-0_6

    2011 doi

  39. [48]

    Loos, David W

    Sarah M. Loos, David W. Renshaw, and André Platzer. 2013. Formal Verification of Distributed Aircraft Controllers. In Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC’13, Philadelphia, PA, USA, April 8-13, 2013 , Calin Belta and Franjo Ivancic (Eds.). ACM,...

    2013

  40. [49]

    Gregory Malecha and Jesper Bengtson. 2015. Rtac: A Fully Reflective Tactic Language. In CoqPL’15

    2015

  41. [50]

    Daniel Matichuk, Toby Murray, and Makarius Wenzel. 2016. Eisbach: A Proof Method Language for Isabelle. J. Autom. Reason. 56, 3 (March 2016), 261–282. https://doi.org/10.1007/s10817-015-9360-2

    2016 doi

  42. [51]

    Stefan Mitsch, Khalil Ghorbal, and André Platzer. 2013. On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles. In Robotics: Science and Systems IX, Technische Universität Berlin, Berlin, Germany, June 24 - June 28, 2013, Paul Newman, Dieter Fox, and David ...

    2013

  43. [52]

    Stefan Mitsch and André Platzer. 2016. The KeYmaera X proof IDE: Concepts on usability in hybrid systems theorem proving. In 3rd Workshop on Formal Integrated Development Environment (EPTCS) , Catherine Dubois, Dominique Mery, and Paolo Masci (Eds.), Vol. 240. 67–81. https://d...

    2016 doi

  44. [53]

    Andreas Müller, Stefan Mitsch, and André Platzer. 2015. Verified Traffic Networks: Component-Based Verification of Cyber-Physical Flow Systems. In ITSC. 757–764. https://doi.org/10.1109/ITSC.2015.128

    2015 doi

  45. [54]

    Tobias Nipkow. 2002. Hoare Logics in Isabelle/HOL . Springer Netherlands, Dordrecht, 341–367. https://doi.org/10.1007/ 978-94-010-0413-8_11

    2002

  46. [55]

    Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle/HOL: A Proof Assistant for Higher-order Logic . Springer-Verlag, Berlin, Heidelberg

    2002

  47. [56]

    Susan Owicki and David Gries. 1976. An axiomatic proof technique for parallel programs I. Acta Informatica 6, 4 (dec 1976), 319–340. https://doi.org/10.1007/BF00268134

    1976 doi

  48. [57]

    Susan S. Owicki. 1975. Axiomatic Proof Techniques for Parallel Programs . Garland Publishing, New York

    1975

  49. [58]

    André Platzer. 2007. Differential Dynamic Logic for Verifying Parametric Hybrid Systems.. In TABLEAUX (LNCS), Nicola Olivetti (Ed.), Vol. 4548. Springer, 216–232. https://doi.org/10.1007/978-3-540-73099-6_17

    2007 doi

  50. [59]

    André Platzer. 2007. Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems, In International Workshop on Hybrid Logic, HyLo’06, Seattle, USA, Proceedings, Patrick Blackburn, Thomas Bolander, Torben Braüner, Valeria de Paiva, and Jørgen Villadsen (Eds.). Electr. Notes Theor...

    2007 doi

  51. [60]

    André Platzer. 2008. Differential Dynamic Logic for Hybrid Systems. J. Autom. Reasoning 41, 2 (2008), 143–189. https://doi.org/10.1007/s10817-008-9103-8

    2008 doi

  52. [61]

    André Platzer. 2010. Differential-algebraic Dynamic Logic for Differential-algebraic Programs. J. Log. Comput. 20, 1 (2010), 309–352. https://doi.org/10.1093/logcom/exn070

    2010 doi

  53. [62]

    André Platzer. 2011. The Structure of Differential Invariants and Differential Cut Elimination. Logical Methods in Computer Science 8, 4 (2011). https://doi.org/10.2168/LMCS-8(4:16)2012

    2011 doi

  54. [63]

    André Platzer. 2012. A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems. Logical Methods in Computer Science 8, 4 (2012). https://doi.org/10.2168/LMCS-8(4:17)2012

    2012 doi

  55. [64]

    André Platzer. 2012. Logics of Dynamical Systems. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012 . IEEE Computer Society, 13–24. https://doi.org/10. 1109/LICS.2012.13

    2012

  56. [65]

    André Platzer. 2015. A Uniform Substitution Calculus for Differential Dynamic Logic. InCADE (LNCS), Amy P. Felty and Aart Middeldorp (Eds.), Vol. 9195. Springer, 467–481. https://doi.org/10.1007/978-3-319-21401-6_32 arXiv:1503.01981

    2015 arXiv

  57. [66]

    André Platzer. 2016. A Complete Uniform Substitution Calculus for Differential Dynamic Logic. J. Autom. Reas. (2016). https://doi.org/10.1007/s10817-016-9385-1

    2016 doi

  58. [67]

    André Platzer and Edmund M. Clarke. 2009. Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. In FM (LNCS), Ana Cavalcanti and Dennis Dams (Eds.), Vol. 5850. Springer, 547–562. https://doi.org/10. 1007/978-3-642-05089-3_35

    2009

  59. [68]

    André Platzer and Jan-David Quesel. 2008. KeYmaera: A Hybrid Theorem Prover for Hybrid Systems.. In IJCAR (LNCS), Alessandro Armando, Peter Baumgartner, and Gilles Dowek (Eds.), Vol. 5195. Springer, 171–178. https: //doi.org/10.1007/978-3-540-71070-7_15

    2008 doi

  60. [69]

    André Platzer and Jan-David Quesel. 2009. European Train Control System: A Case Study in Formal Verification. In ICFEM (LNCS), Karin Breitman and Ana Cavalcanti (Eds.), Vol. 5885. Springer, 246–265. https://doi.org/10.1007/ 978-3-642-10373-5_13

    2009

  61. [70]

    Vaughan R. Pratt. 1976. Semantical Considerations on Floyd-Hoare Logic. In 17th Annual Symposium on Foundations of Computer Science, Houston, Texas, USA, 25-27 October 1976 . IEEE Computer Society, 109–121. https://doi.org/10.1109/ SFCS.1976.27

    1976

  62. [71]

    Piotr Rudnicki. 1987. Obvious Inferences. J. Autom. Reasoning 3, 4 (1987), 383–393. https://doi.org/10.1007/BF00247436

    1987 doi

  63. [72]

    Antonis Stampoulis and Zhong Shao. 2010. VeriML: typed computation of logical terms inside a language with effects. In Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010 , Paul Hudak...

    2010

  64. [73]

    Antonis Stampoulis and Zhong Shao. 2012. Static and user-extensible proof checking. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, John Field and Michael Hicks (Ed...

    2012

  65. [74]

    Kohei Suenaga and Ichiro Hasuo. 2011. Programming with Infinitesimals: A While-Language for Hybrid System Modeling. In Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II (Lecture Notes in C...

    2011 doi

  66. [75]

    Donald Syme. 1997. DECLARE: A Prototype Declarative Proof System for Higher Order Logic

    1997

  67. [76]

    The Coq Development Team. 2017. Coq Proof Assistant. (2017). http://coq.inria.fr/ Accessed: 2017-05-25

    2017

  68. [77]

    Christoph Traut and Lars Noschinski. 2014. Pattern-based Subterm Selection in Isabelle. In Proceedings of Isabelle Workshop 2014

    2014

  69. [78]

    Markus Wenzel. 1999. Isar - A Generic Interpretative Approach to Readable Formal Proof Documents. In Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99, Nice, France, September, 1999, Proceedings (Lecture Notes in Computer Science) , Yves Bertot, ...

    1999 doi

  70. [79]

    Makarius Wenzel. 2006. Structured Induction Proofs in Isabelle/Isar. In Mathematical Knowledge Management, 5th International Conference, MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings (Lecture Notes in Computer Science), Jonathan M. Borwein and William M. Farmer (Eds...

    2006 doi

  71. [80]

    Makarius Wenzel. 2007. Isabelle/Isar – a generic framework for human-readable proof documents. In UNIVERSITY OF BIAŁYSTOK

    2007

  72. [81]

    Markus Wenzel and Freek Wiedijk. 2002. A Comparison of Mizar and Isar. J. Autom. Reasoning 29, 3-4 (2002), 389–411. https://doi.org/10.1023/A:1021935419355

    2002 doi

  73. [82]

    Freek Wiedijk. 2001. Mizar Light for HOL Light. InTheorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings (Lecture Notes in Computer Science) , Richard J. Boulton and Paul B. Jackson (Eds.), ...

    2001 doi

  74. [83]

    Krishnaswami, Aleksandar Nanevski, and Viktor Vafeiadis

    Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, and Viktor Vafeiadis. 2013. Mtac: A Monad for Typed Tactic Programming in Coq. SIGPLAN Not. 48, 9 (Sept. 2013), 87–100. https://doi.org/10.1145/ 2544174.2500579 , Vol. 1, No. 1, Article 1. Publicatio...

    2013

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.