Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2605.10188 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866917479896317952 |
|---|---|
| author | Hellwig, Jonathan Qian, Long Platzer, André |
| author_facet | Hellwig, Jonathan Qian, Long Platzer, André |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_10188 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Deductive Refinement Calculus for Differential-Algebraic Programs Hellwig, Jonathan Qian, Long Platzer, André Logic in Computer Science 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. |
| title | A Deductive Refinement Calculus for Differential-Algebraic Programs |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2605.10188 |