Abstract This paper presents differential-algebraic refinement logic () with which one can deductively verify both properties and relations of differential-algebraic programs (DAPs) that extend hybrid dynamical systems with differential-algebraic equations (DAEs). A refinement calculus is introduced that enables the sound comparison of trajectories of differential-algebraic equations, crucially utilizing a novel trace-based semantics. This enables the incremental verification/simplification of complicated DAEs, while ensuring correctness at each step by the soundness of the calculus. The calculus is shown to certify index reductions of DAEs, providing trustworthy syntactic proofs of correctness at each step of the reduction.

Abstract This paper introduces a novel axiomatic proof calculus for differential-algebraic dynamic logic (). The calculus enables deductive verification and sound transformation of differential-algebraic programs (DAPs), which generalize differential-algebraic equations, while remaining compatible with differential dynamic logic () for hybrid programs. One central contribution is the ghost switching axiom which establishes precise conditions to decompose multi-modal DAPs into equivalent hybrid systems with ordinary differential equations. The applicability of the calculus is demonstrated through a formal equivalence proof, showing the reduction of the Euclidean pendulum from a differential-algebraic formulation to an equivalent system of ordinary differential equations.