4 citations · 5 across the 11 of their papers we have counts for
6 papers · 2 filters
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…