Numerical invariants through convex relaxation and max-strategy iteration

DOI10.1007/s10703-013-0190-8zbMath1291.68256arXiv1204.1147OpenAlexW1984562692MaRDI 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 optimizationsystems verificationfixpoint algorithms

Mathematics Subject Classification ID

Convex programming (90C25) Fixed-point theorems (47H10) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

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

This page was built for publication: Numerical invariants through convex relaxation and max-strategy iteration