Numerical invariants through convex relaxation and max-strategy iteration
From MaRDI portal
Publication:2248100
DOI10.1007/s10703-013-0190-8zbMath1291.68256arXiv1204.1147MaRDI QIDQ2248100
Thomas Martin Gawlitza, Helmut Seidl
Publication date: 30 June 2014
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1204.1147
90C25: Convex programming
47H10: Fixed-point theorems
68Q60: Specification and verification (program logics, model checking, etc.)
Uses Software
Cites Work
- Unnamed Item
- Abstract interpretation meets convex optimization
- ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
- The octagon abstract domain
- A lattice-theoretical fixpoint theorem and its applications
- Template-Based Unbounded Time Verification of Affine Hybrid Automata
- A generic ellipsoid abstract domain for linear time invariant systems
- Discretizing Affine Hybrid Automata with Uncertainty
- Semidefinite optimization
- A Policy Iteration Technique for Time Elapse over Template Polyhedra
- Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis
- Exponential Lower Bounds for Policy Iteration
- Precise Relational Invariants Through Strategy Iteration
- Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely
- Proving Termination by Policy Iteration
- Hybrid Systems: Computation and Control
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- Precise Fixpoint Computation Through Strategy Iteration
