A Deductive Refinement Calculus for Differential-Algebraic Programs

TL;DR

This paper introduces a new deductive refinement calculus for verifying properties of differential-algebraic programs, enhancing the correctness and simplification of complex DAEs.

Contribution

It presents a novel trace-based semantics and a refinement calculus that enables sound, incremental verification and index reduction of differential-algebraic equations.

Findings

Enables sound comparison of DAE trajectories

Supports incremental verification and simplification of DAEs

Provides complete certification of index reductions

Abstract

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.