arXiv subjects

André Platzer

Publications and source records attributed to André Platzer.

At least 19 recordsLinked to original sources

arXiv2026

LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Games

Hybrid games model cyber-physical systems (CPS), like cars, trains, and airplanes, where discrete control decisions interact with continuous physical dynamics. We use Large Language Models (LLMs) to scale formal verification and synthesis for hybrid systems and games for a high-level hybrid games symbolic logic, differential game logic (dGL). This combination of a logic with the right expressivity and automation of the interactive theorem proving process using LLMs brings within reach a challenging class of CPS verification/synthesis problems, that were previously well out of range of automatic theorem proving. We demonstrate it on five challenging case studies, all beyond the reach of existing automatic techniques. Verification succeeds for all five, and the synthesis of control solutions succeeds for four of the five.

cs.LO↗

arXiv2026

Differential Equations as Fixpoints and Games

Games and fixpoints are unified by proving that first-order game logic GL and the first-order modal mu-calculus L_mu are proved to be equiexpressive and equivalent, thereby fully aligning their expressive and deductive power. That is, there is a semantics-preserving translation from GL to L_mu, and vice versa. And both translations are provability-preserving, while equivalence with there-and-back-again roundtrip translations are provable in both calculi. This is to be contrasted with the propositional case, where game logic is strictly less expressive than the modal mu-calculus (without adding sabotage games). The extensions with differential equations, differential game logic (dGL) and differential modal mu-calculus, are also proved equiexpressive and equivalent. Moreover, as the continuous dynamics are definable by fixpoints or via games, ODEs can be axiomatized completely and, as a consequence, infinitesimally robust properties of ODEs can be decided via proof search. Rational gameplay provably collapses the games into single-player games to yield a strong arithmetical completeness theorem for dGL with rational-time ODEs.

cs.LO↗

arXiv2026

Comparison Invariants for Verifying Control Invariance

Control invariance validates that dynamical systems have a control input that preserves a given property at all times. This paper introduces a set of sound axioms and proof rules in differential dynamic logic (dL) that enable verification of control invariance. First, the scalar and vector comparison principles, relating a system of differential equations to a comparison system such that invariance properties can be established more easily, are axiomatized in dL. This axiomatization primarily utilizes differential ghosts, which are proof-theoretic generalizations of comparison systems. Next, with the comparison principles serving as the basis, comparison invariants are introduced, and sound axioms and proof rules are derived. Comparison invariants reduce the question of control invariance to a functional inequality on its Lie derivative for a suitable class of functions, moreover, the right choice of function can result in decidable arithmetic. Furthermore, the perennially popular control barrier functions (CBFs) used in safety-critical control are shown to be a special instance of comparison invariants. This yields an axiomatization of CBFs that leads to a dedicated set of proof rules. The rules allow for the verification of CBFs, which are traditionally used for synthesizing safe controllers without verification. Lastly, comparison invariants are shown to unify several other safety verification techniques, including Darboux invariants and differential invariants, further cementing their versatility.

cs.LO↗

arXiv2026

Three-player Differential Game Logic

This paper introduces the three-player differential game logic dGL3, which enables the verification of hybrid games of discrete and differential equation dynamics with three players who may or may not form coalitions. Each player has an individual goal they try to fulfill, so the game becomes non-zero-sum when the goals of the players overlap. This is how dGL3 can verify complex situations involving multiple players, taking into account their coalitional power. dGL3 excels at verifying games where players share safety objectives but otherwise pursue different goals, so that they may or may not collaborate. In this case, zero-sum assumptions lead to overly conservative results by neglecting the potential of coordination amongst the players. In this paper, the syntax and semantics of dGL3 are presented and crucial properties of dGL3 are proved. A sound and relatively complete proof calculus for dGL3 is introduced and the use of dGL3 is illustrated in a canonical example.

cs.LO↗

arXiv2026

Subreflexive Logic: Completeness without Identity

This paper shows that the substructural logic without the identity principle A->A (i.e., subreflexive logic) has principled sound and complete semantics and supports a variety of applications. This decidable generalization of propositional logic naturally interprets implication as robust consequence. Subreflexive logic is proved to admit syntactic cut elimination. Heyting and Boolean semialgebras are introduced as generalizations of Heyting and Boolean algebras and are shown to provide complete algebraic semantics without inadvertently reintroducing reflexivity. Semi-adjunctions on semi-categories and (identity-free) (co-)units are defined to give complete semi-categorical semantics. In the classical case, denotational set semantics that interpret implication as robust material implication are proved complete for subreflexive logic.

cs.LO↗

arXiv2026

Complete Robust Hybrid Systems Reachability

This paper introduces robust differential dynamic logic (a fragment of differential dynamic logic) to specify and reason about robust hybrid systems. Practically meaningful syntactic restrictions naturally ensure that definable properties are topologically open and thus by construction robust with respect to infinitesimal perturbations, without explicit quantitative margins of error in the syntax or in proofs. The main result is a proof of absolute completeness of robust differential dynamic logic for reachability properties of general hybrid systems. This is the first absolute completeness proof for hybrid systems with exact semantics. The proof is constructive, self-contained, and demonstrates how robustly correct hybrid systems reachability specifications can be automatically verified through proof.

cs.LO↗

arXiv2026

Differential Equation Inductive Robustness Axiomatization

This article establishes the completeness of an axiomatization for the robust safety of dynamical systems with polynomial differential equations on bounded time horizons. Safety properties of robust systems are uniformly reduced to a sound axiomatization of polynomial invariants, resulting in reliable logical proofs of correctness. Approximate decidability results are also established: there is a computable algorithm such that, given any perturbation parameter $δ$, it either produces a symbolic proof of robust safety (hence correctly decides the dynamical system to be robustly safe), or correctly decides that the system is not robustly safe under a perturbation of level $δ$. In contrast to earlier works, this article crucially leverages results from subanalytic geometry to retain a level of exactness, thereby establishing positive results of provability/decidability allowing for arbitrary bounded (semialgebraic) initial/post conditions even without positive separation at their (topological) boundaries. This enables the generation of proofs of inductive safety beyond finite time horizons for general hybrid dynamical systems.

cs.LO↗

arXiv2026

Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements

Cyber-physical systems are inherently complex due to their connection between software and the physical world. Iterative design reduces their complexity, but increases the need to repeatedly recheck their safety in full after every change. We introduce the refactoring-as-propositions principle in which refactorings are represented as propositions along with a method for proving that system refactorings preserve their required properties by transferring the proof along the respective modification. It is based on differential refinement logic (dRL), with which one can simultaneously and rigorously refer to properties of the systems and the relation between a refactored system and its original version. Refinements represent a uniform way of expressing different types of hybrid system refactorings, including those that introduce auxiliary variables. Furthermore, we show how these refactorings can be proved automatically, and/or reduce to a modular proof solely about the local change rather than about the whole system.

cs.LO↗

arXiv2026

A Deductive Refinement Calculus for Differential-Algebraic Programs

This paper presents differential-algebraic refinement logic (dARL) with which one can deductively verify both properties and relations of differential-algebraic programs (DAPs) that extend hybrid dynamical systems with differential-algebraic equations (DAEs). A refinement calculus is introduced that enables the sound comparison of trajectories of differential-algebraic equations, crucially utilizing a novel trace-based semantics. This enables the incremental verification/simplification of complicated DAEs, while ensuring correctness at each step by the soundness of the calculus. The calculus is shown to be complete for certifying index reductions of DAEs, providing trustworthy syntactic proofs of correctness at each step of the reduction.

cs.LO↗

arXiv2026

Heterogeneous Dynamic Logic: Provability Modulo Program Theories

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

cs.LO↗

arXiv2026

Differential Elimination and Algebraic Invariants of Polynomial Dynamical Systems

Invariant sets are a key ingredient for verifying safety and other properties of cyber-physical systems that mix discrete and continuous dynamics. We adapt the elimination-theoretic Rosenfeld-Gröbner algorithm to systematically obtain algebraic invariants of polynomial dynamical systems without using Gröbner bases or quantifier elimination. We identify totally real varieties as an important class for efficient invariance checking.

cs.SC↗

arXiv2026

Oracular Programming: A Modular Foundation for Building LLM-Enabled Software

Large Language Models (LLMs) can solve previously intractable tasks given only natural-language instructions and a few examples, but they remain difficult to steer precisely and lack a key capability for building reliable software at scale: the modular composition of computations under enforceable contracts. As a result, they are often embedded in larger software pipelines that use domain-specific knowledge to decompose tasks and improve reliability through validation and search. Yet the complexity of writing, tuning, and maintaining such pipelines has so far limited their sophistication. We propose oracular programming: a foundational paradigm for integrating traditional, explicit computations with inductive oracles such as LLMs. It rests on two directing principles: the full separation of core and search logic (allowing the latter to freely evolve without breaking the former), and the treatment of few-shot examples as grounded and evolvable program components. Within this paradigm, programmers express high-level problem-solving strategies as programs with unresolved choice points. These choice points are resolved at runtime by LLMs, which generalize from user-provided examples of correct and incorrect decisions. An oracular program is composed of three orthogonal components: a strategy that consists of a nondeterministic program with choice points that can be reified into a search tree, a policy that specifies how to navigate this tree with the help of LLM oracles, and a set of demonstrations that describe successful and unsuccessful tree navigation scenarios across diverse problem instances. Each component is expressed in a dedicated programming language. We address the key programming language design challenges of modularly composing oracular programs and enforcing consistency between their components as they evolve.

cs.PL↗

arXiv2025

Can Large Language Models Autoformalize Kinematics?

Autonomous cyber-physical systems like robots and self-driving cars could greatly benefit from using formal methods to reason reliably about their control decisions. However, before a problem can be solved it needs to be stated. This requires writing a formal physics model of the cyber-physical system, which is a complex task that traditionally requires human expertise and becomes a bottleneck. This paper experimentally studies whether Large Language Models (LLMs) can automate the formalization process. A 20 problem benchmark suite is designed drawing from undergraduate level physics kinematics problems. In each problem, the LLM is provided with a natural language description of the objects' motion and must produce a model in differential game logic (dGL). The model is (1) syntax checked and iteratively refined based on parser feedback, and (2) semantically evaluated by checking whether symbolically executing the dGL formula recovers the solution to the original physics problem. A success rate of 70% (best over 5 samples) is achieved. We analyze failing cases, identifying directions for future improvement. This provides a first quantitative baseline for LLM-based autoformalization from natural language to a hybrid games logic with continuous dynamics.

cs.LO↗

arXiv2025

From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes

Synthesizing controllers that enforce both safety and actuator constraints is a central challenge in the design of cyber-physical systems. State-of-the-art reachability methods based on zonotopes deliver impressive scalability, yet no zonotope reachability tool has been formally verified and the lack of end-to-end correctness undermines the confidence in their use for safety-critical systems. Although deductive verification with the hybrid system prover KeYmaera X could, in principle, resolve this assurance gap, the high-dimensional set representations required for realistic control envelopes overwhelm its reasoning based on quantifier elimination. To address this gap, we formalize how control-invariant sets serve as sound safety certificates. Building on that foundation, we develop a verification pipeline for control envelopes that unites scalability and formal rigor. First, we compute control envelopes with high-performance reachability algorithms. Second, we certify every intermediate result using provably correct logical principles. To accelerate this certification, we offload computationally intensive zonotope containment tasks to efficient numerical backends, which return compact witnesses that KeYmaera X validates rapidly. We show the practical utility of our approach through representative case studies.

cs.LO↗

arXiv2025

Complete Dynamic Logic of Communicating Hybrid Programs

This article presents a relatively complete proof calculus for the dynamic logic of communicating hybrid programs dLCHP. Beyond hybrid systems, communicating hybrid programs not only feature mixed discrete and continuous dynamics but also their parallel interactions in parallel hybrid systems. This not only combines the subtleties of hybrid and discrete parallel systems, but parallel hybrid dynamics necessitates that all parallel subsystems synchronize in time and evolve truly simultaneously. To enable compositional reasoning nevertheless, dLCHP combines differential dynamic logic dL with mutual abstraction of subsystems by assumption-commitment (ac) reasoning. The resulting proof calculus preserves the essence of dynamic logic axiomatizations, while revealing-and being driven by-a new modal logic view onto ac-reasoning. The dLCHP proof calculus is shown to be complete relative to $Ω$-FOD, the first-order logic of differential equation properties FOD augmented with communication traces. This confirms that the calculus covers all aspects of parallel hybrid systems, because it lacks no axioms to reduce all their dynamical effects to the assertion logic. Additional axioms for encoding communication traces enable a provably correct equitranslation between $Ω$-FOD and FOD, which reveals the possibility of representational succinctness in parallel hybrid systems proofs. Transitively, this establishes a full proof-theoretical alignment of dLCHP and dL, and shows that reasoning about parallel hybrid systems is exactly as hard as reasoning about hybrid systems, continuous systems, or discrete systems.

cs.LO↗

arXiv2025

Hybrid Game Control Envelope Synthesis

Control problems for embedded systems like cars and trains can be modeled by two-player hybrid games. Control envelopes, which are families of safe control solutions, correspond to nondeterministic winning policies of hybrid games, where each deterministic specialization of the policy is a control solution. This paper synthesizes nondeterministic winning policies for hybrid games that are as permissive as possible. It introduces subvalue maps, a compositional representation of such policies that enables verification and synthesis along the structure of the game. An inductive logical characterization in differential game logic (dGL) checks whether a subvalue map induces a sound control envelope which always induces a winning play. A policy is said to win if it always achieves the desirable outcome when the player follows it, no matter what actions the opponent plays. The maximal subvalue map, which allows the most action options while still winning, is shown to exist and satisfy a logical characterization. A family of algorithms for nondeterministic policy synthesis can be obtained from the inductive subvalue map soundness characterization. An implementation of these findings is evaluated on examples that use the expressivity of dGL to model a range of diverse control challenges.

cs.PL↗

arXiv2025

Semi-Competitive Differential Game Logic

This paper introduces semi-competitive differential game logic dGLsc, which enables verification of safety-critical applications that involve interactions between two agents. In dGLsc, these interactions are specified as games on hybrid systems with two players that may collaborate with each other when helpful and may compete when necessary. The players in the hybrid games of dGLsc have individual goals that may overlap, leading to nonzero-sum games. This makes dGLsc especially well-suited for verifying situations where players, e.g., share safety objectives but otherwise pursue different goals, so that zero-sum assumptions lead to overly conservative results. Additionally, dGLsc solves the subtlety that even though each player may benefit from knowledge of the other player's goals, e.g., concerning shared safety objectives, unsafe situations might still occur if every player were to mutually assume the other player would act to avoid unsafety. The syntax and semantics, as well as a sound and relatively complete proof calculus are presented for dGLsc. The relationship between dGLsc and zero-sum differential game logic dGL is discussed and the purpose of dGLsc illustrated in a canonical example.

cs.LO↗

arXiv2025

Approximate Axiomatization for Differentially-Defined Functions

This article establishes a complete approximate axiomatization for the real-closed field $\mathbb{R}$ expanded with all differentially-defined functions, including special functions such as $\sin(x), \cos(x), e^x, \dots$. Every true sentence is provable up to some numerical approximation, and the truth of such approximations converge under mild conditions. Such an axiomatization is a fragment of the axiomatization for differential dynamic logic, and is therefore a finite extension of the axiomatization of real-closed fields. Furthermore, the numerical approximations approximate formulas containing special function symbols by $\text{FOL}_{\mathbb{R}}$ formulas, improving upon earlier decidability results only concerning closed sentences.

cs.LO↗