4 citations · 5 across the 11 of their papers we have counts for
11 papers · 1 filter
Comparison Invariants for Verifying Control Invariance
Promit Panja, André Platzer
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 i…
Subreflexive Logic: Completeness without Identity
Noah Abou El Wafa, André Platzer
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 a…
Differential Equation Inductive Robustness Axiomatization
André Platzer, Long Qian
This article establishes the completeness of an axiomatization for the robust safety of dynamical systems with polynomial differential equations on bounded time horizons. Safety pr…
Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements
Enguerrand Prebet, André Platzer
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…
A Deductive Refinement Calculus for Differential-Algebraic Programs
Jonathan Hellwig, Long Qian, André Platzer
This paper presents differential-algebraic refinement logic (dARL) with which one can deductively verify both properties and relations of differential-algebraic programs (DAPs) tha…
Complete Robust Hybrid Systems Reachability
Noah Abou El Wafa, André Platzer
This paper introduces robust differential dynamic logic (a fragment of differential dynamic logic) to specify and reason about robust hybrid systems. Practically meaningful syntact…
From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes
Jonathan Hellwig, Lukas Schäfer, Long Qian +2
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 bas…
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
Samuel Teuber, Mattias Ulbrich, André Platzer +1
Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL),…
Approximate Axiomatization for Differentially-Defined Functions
André Platzer, Long Qian
This article establishes a complete approximate axiomatization for the real-closed field expanded with all differentially-defined functions, including special function…
A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
Jonathan Hellwig, André Platzer
This paper introduces a proof calculus for real-analytic differential-algebraic dynamic logic, enabling correct transformations of differential-algebraic equations. Applications in…
Axiomatization of Compact Initial Value Problems: Open Properties
André Platzer, Long Qian
This article proves the completeness of an axiomatization for initial value problems (IVPs) with compact initial conditions and compact time horizons for bounded open safety, open…