The Structure of Differential Invariants and Differential Cut Elimination

DOI10.2168/LMCS-8(4:16)2012zbMath1261.03112arXiv1104.1987MaRDI QIDQ4899116

André Platzer

Publication date: 7 January 2013

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1104.1987

zbMATH Keywords

verificationhybrid systemsdifferential equationsproof theorydifferential invariantsdifferential dynamic logiclogics of programsdifferential cut eliminationproof search complexityreal differential semialgebraic geometry

Mathematics Subject Classification ID

Symmetries, invariants of ordinary differential equations (34C14) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Cut-elimination and normal-form theorems (03F05) Hybrid systems of ordinary differential equations (34A38)

Related Items (8)

Differential Game Logic ⋮ Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Verification of Hybrid Systems ⋮ Change-of-bases abstractions for non-linear hybrid systems ⋮ A complete uniform substitution calculus for differential dynamic logic ⋮ A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets ⋮ Vector barrier certificates and comparison systems ⋮ Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants

Uses Software

• PHAVer
• HyTech
• ETPS

This page was built for publication: The Structure of Differential Invariants and Differential Cut Elimination