Abstract interpretation meets convex optimization
From MaRDI portal
Publication:435969
DOI10.1016/j.jsc.2011.12.048zbMath1246.90118OpenAlexW2153421566MaRDI QIDQ435969
Thomas Martin Gawlitza, Helmut Seidl, Stéphane Gaubert, Assalé Adjé, Eric Goubault
Publication date: 13 July 2012
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jsc.2011.12.048
convex optimizationstatic analysisabstract interpretationsemi-definite relaxationfixpoint equationsstrategy improvement algorithms
Related Items
Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case ⋮ Automatic synthesis of \(k\)-inductive piecewise quadratic invariants for switched affine control programs ⋮ Numerical invariants through convex relaxation and max-strategy iteration ⋮ Computing the smallest fixed point of order-preserving nonexpansive mappings arising in positive stochastic games and static analysis of programs
Uses Software
Cites Work
- Solving semidefinite-quadratic-linear programs using SDPT3
- Large-scale semidefinite programs in electronic structure calculation
- Programming languages and systems. 16th European symposium of programming, ESOP 2007, held as part of the joint European conferences on theory and practice of software, ETAPS 2007, Braga, Portugal, March 24 -- April 1, 2007. Proceedings.
- Implementation of a primal-dual method for SDP on a shared memory parallel architecture
- Quadratic programming is in NP
- Semidefinite optimization
- Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis
- Precise Relational Invariants Through Strategy Iteration
- SDPT3 — A Matlab software package for semidefinite programming, Version 1.3
- CSDP 2.3 user's guide
- CSDP, A C library for semidefinite programming
- Using SeDuMi 1.02, A Matlab toolbox for optimization over symmetric cones
- Implementation and evaluation of SDPA 6.0 (Semidefinite Programming Algorithm 6.0)
- Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- Static Analysis by Policy Iteration on Relational Domains
- Precise Fixpoint Computation Through Strategy Iteration
- Verification, Model Checking, and Abstract Interpretation
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Abstract interpretation meets convex optimization
