Numerical invariants through convex relaxation and max-strategy iteration

DOI10.1007/S10703-013-0190-8MaRDI QIDQ2248100zbMATH OpenOpenAlexFDO

Authors 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)

Abstract: In this article we develop a max-strategy improvement algorithm for computing least fixpoints of operators on on the reals that are point-wise maxima of finitely many monotone and order-concave operators. Computing the uniquely determined least fixpoint of such operators is a problem that occurs frequently in the context of numerical program/systems verification/analysis. As an example for an application we discuss how our algorithm can be applied to compute numerical invariants of programs by abstract interpretation based on quadratic templates.

Recommendations

• Abstract interpretation meets convex optimization
• Precise Relational Invariants Through Strategy Iteration
• Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
• Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
• Computing relaxed abstract semantics w.r.t. quadratic zones precisely

Cites work

• scientific article; zbMATH DE number 1738295 (Why is no real title available?)
• A Policy Iteration Technique for Time Elapse over Template Polyhedra
• A generic ellipsoid abstract domain for linear time invariant systems
• A lattice-theoretical fixpoint theorem and its applications
• Abstract interpretation meets convex optimization
• Computer Aided Verification
• Computing relaxed abstract semantics w.r.t. quadratic zones precisely
• Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
• Discretizing affine hybrid automata with uncertainty
• Exponential lower bounds for policy iteration
• Hybrid Systems: Computation and Control
• Precise Fixpoint Computation Through Strategy Iteration
• Precise Relational Invariants Through Strategy Iteration
• Proving termination by policy iteration
• Semidefinite optimization
• Template-based unbounded time verification of affine hybrid automata
• The octagon abstract domain
• Verification, Model Checking, and Abstract Interpretation
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs

Cited in

(1)

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

Describes a project that uses

Uses Software

• LUSTRE

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

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