A Deductive Refinement Calculus for Differential-Algebraic Programs
2026-05-11 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors present dARL, a logic system to check and compare programs involving both differential and algebraic equations, which are more complex than usual hybrid systems. They introduce a method to compare how solutions to these equations behave over time in a way that can be trusted. Their approach allows breaking down complicated equations into simpler parts step-by-step, ensuring each step is correct. They also prove that their method is complete for verifying a common simplification technique called index reduction.
differential-algebraic equationsrefinement calculushybrid dynamical systemstrace-based semanticstrajectory comparisonincremental verificationindex reductionsoundnesscompleteness
Authors
Jonathan Hellwig, Long Qian, André Platzer
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.