A Deductive Refinement Calculus for Differential-Algebraic Programs
For researchers working on hybrid systems and differential-algebraic equations, this provides a formal method for trustworthy incremental verification of complex DAEs.
The paper introduces differential-algebraic refinement logic (dARL) for deductive verification of differential-algebraic programs, enabling sound comparison of trajectories and incremental verification. The calculus is complete for certifying index reductions of DAEs.
This paper presents differential-algebraic refinement logic (dARL) 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 be complete for certifying index reductions of DAEs, providing trustworthy syntactic proofs of correctness at each step of the reduction.