Numerical invariants through convex relaxation and max-strategy iteration

DOI10.1007/S10703-013-0190-8zbMATH Open1291.68256arXiv1204.1147OpenAlexW1984562692MaRDI QIDQ2248100FDOQ2248100

Thomas Martin Gawlitza, Helmut Seidl

Publication date: 30 June 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1204.1147

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

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)

Cites Work

• The octagon abstract domain
• A lattice-theoretical fixpoint theorem and its applications
• Semidefinite optimization
• Hybrid Systems: Computation and Control
• Title not available (Why is that?)
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• Computer Aided Verification
• Precise Fixpoint Computation Through Strategy Iteration
• Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
• Precise Relational Invariants Through Strategy Iteration
• Abstract interpretation meets convex optimization
• Computing relaxed abstract semantics w.r.t. quadratic zones precisely
• Verification, Model Checking, and Abstract Interpretation
• A generic ellipsoid abstract domain for linear time invariant systems
• Template-Based Unbounded Time Verification of Affine Hybrid Automata
• Discretizing Affine Hybrid Automata with Uncertainty
• Exponential lower bounds for policy iteration
• A Policy Iteration Technique for Time Elapse over Template Polyhedra
• Proving Termination by Policy Iteration

Cited In (1)

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

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)