Numerical invariants through convex relaxation and max-strategy iteration

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

zbMATH Keywords

convex optimization; systems verification; fixpoint algorithms

Mathematics Subject Classification ID

90C25: Convex programming

47H10: Fixed-point theorems

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Counterexample- and simulation-guided floating-point loop invariant synthesis

Uses Software

• LUSTRE

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