Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
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…
cs.LO2025
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…
cs.LO2025
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…