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.

翻译：本文提出微分代数精化逻辑(dARL)，可对微分代数程序(DAPs)的性质与关系进行演绎验证，此类程序通过微分代数方程(DAEs)扩展了混合动力系统。文中引入一种精化演算，该演算通过创新性地利用基于迹的语义，能够对微分代数方程的轨迹进行可靠比较。这使复杂DAEs的增量式验证/简化成为可能，同时通过演算的可靠性确保每一步的正确性。本文证明该演算在验证DAEs指标约简方面具有完备性，为约简过程的每一步提供了可信的语法正确性证明。