9 papers
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…
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),…
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…