Axiomatization of compact initial value problems: open properties

DOI10.1145/3763228MaRDI QIDQ6869435zbMATH OpenFDO

Authors André Platzer, Long Qian

Publication date 22 January 2026

Published in Journal of the ACM (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1145/3763228

zbMATH Keywords

differential dynamic logicdifferential equation axiomatizationinvariants

Mathematics Subject Classification ID

Logic in computer science (03B70) Computation over the reals, computable analysis (03D78) Nonlinear ordinary differential equations and systems (34A34) Theoretical approximation of solutions to ordinary differential equations (34A45)

Cites work

• A complete uniform substitution calculus for differential dynamic logic
• A computable and compositional semantics for hybrid automata
• A Coq formalization of Taylor models and power series for solving ordinary differential equations
• A Universal Ordinary Differential Equation
• A verified ODE solver and the Lorenz attractor
• An axiomatic approach to existence and liveness for differential equations
• AN EFFECTIVE CAUCHY-PEANO EXISTENCE THEOREM FOR UNIQUE SOLUTIONS
• CAPD::DynSys: a flexible C++ toolbox for rigorous numerical analysis of dynamical systems
• Computability of ordinary differential equations
• Computability, noncomputability and undecidability of maximal intervals of IVPs
• Computing with polynomial ordinary differential equations
• Differential dynamic logic for hybrid systems
• Differential equation axiomatization. The impressive power of differential ghosts
• Differential equation invariance axiomatization
• Direct formal verification of liveness properties in continuous and hybrid dynamical systems
• scientific article; zbMATH DE number 1183917 (Why is no real title available?)
• scientific article; zbMATH DE number 1167864 (Why is no real title available?)
• scientific article; zbMATH DE number 1169378 (Why is no real title available?)
• scientific article; zbMATH DE number 1460545 (Why is no real title available?)
• scientific article; zbMATH DE number 2247480 (Why is no real title available?)
• scientific article; zbMATH DE number 3053259 (Why is no real title available?)
• JuliaReach
• KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
• Logical foundations of cyber-physical systems
• Logics of dynamical systems
• Mémoire sur les courbes définies par une équation différentielle.
• Note on the derivatives with respect to a parameter of the solutions of a system of differential equations.
• Numerical initial value problems in ordinary differential equations.
• On recurrent reachability for continuous linear dynamical systems
• On the complexity of solving initial value problems
• On the Skolem problem for continuous linear dynamical systems
• Ordinary differential equations.
• Pegasus: sound continuous invariant generation
• Reachability in Linear Dynamical Systems
• Rigorous numerical computation of polynomial differential equations over unbounded domains
• Solving discontinuous initial value problems with unique solutions is equivalent to computing over the transfinite
• Stability and robustness analysis of nonlinear systems via contraction metrics and SOS programming
• The Complete Proof Theory of Hybrid Systems
• The continuous Skolem-Pisot problem
• The pseudo-reachability problem for diagonalisable linear dynamical systems
• Turing computability. Theory and applications

This page was built for publication: Axiomatization of compact initial value problems: open properties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6869435)