4 papers
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…
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…
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…
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…