JACM · 2025

Axiomatization of Compact Initial Value Problems: Open Properties

André Platzer and Long Qian^α

Authors listed in alphabetical order.

Journal of the ACM

BibTeX

@article{platzer2025compact,
  title = {Axiomatization of Compact Initial Value Problems: Open Properties},
  author = {André Platzer and Long Qian},
  year = {2025},
  journal = {Journal of the ACM},
  volume = {72},
  number = {6},
  pages = {41:1--41:51},
  doi = {10.1145/3763228},
  eprint = {2410.13836},
  archivePrefix = {arXiv}
}

Overview

A complete axiomatization of open safety, open liveness, and existence properties for compact initial value problems, connecting symbolic proofs with rigorous numerical error bounds.