Abstract interpretation meets convex optimization
From MaRDI portal
Publication:435969
DOI10.1016/J.JSC.2011.12.048zbMATH Open1246.90118OpenAlexW2153421566MaRDI QIDQ435969FDOQ435969
Authors: Thomas Martin Gawlitza, Helmut Seidl, Assalé Adjé, Stéphane Gaubert, Éric 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
Recommendations
- Improving strategies via SMT solving
- Invariant generation through strategy iteration in succinctly represented control flow graphs
- Static Analysis by Policy Iteration on Relational Domains
- Abstract fixpoint computations with numerical acceleration methods
- Fixpoint Computation in the Polyhedra Abstract Domain Using Convex and Numerical Analysis Tools
convex optimizationabstract interpretationstatic analysissemi-definite relaxationfixpoint equationsstrategy improvement algorithms
Cites Work
- CSDP 2.3 user's guide
- CSDP, A C library for semidefinite programming
- SDPT3 — A Matlab software package for semidefinite programming, Version 1.3
- Using SeDuMi 1.02, A Matlab toolbox for optimization over symmetric cones
- Solving semidefinite-quadratic-linear programs using SDPT3
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Semidefinite optimization
- Quadratic programming is in NP
- Implementation and evaluation of SDPA 6.0 (Semidefinite Programming Algorithm 6.0)
- Computer Aided Verification
- Static Analysis by Policy Iteration on Relational Domains
- Precise Fixpoint Computation Through Strategy Iteration
- 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
- Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
- Precise Relational Invariants Through Strategy Iteration
- Computing relaxed abstract semantics w.r.t. quadratic zones precisely
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
- Large-scale semidefinite programs in electronic structure calculation
Cited In (24)
- Logico-numerical max-strategy iteration
- Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
- Improving the results of program analysis by abstract interpretation beyond the decreasing sequence
- Linear absolute value relation analysis
- Narrowing operators on template abstract domains
- Numerical invariants through convex relaxation and max-strategy iteration
- Stratified static analysis based on variable dependencies
- Title not available (Why is that?)
- Acceleration of the abstract fixpoint computation in numerical program analysis
- Template polyhedra and bilinear optimization
- Template polyhedra with a twist
- Computing the smallest fixed point of order-preserving nonexpansive mappings arising in positive stochastic games and static analysis of programs
- Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case
- Descending chains and narrowing on template abstract domains
- Computing relaxed abstract semantics w.r.t. quadratic zones precisely
- Invariant generation through strategy iteration in succinctly represented control flow graphs
- Abstract fixpoint computations with numerical acceleration methods
- Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
- Improving strategies via SMT solving
- Abstract interpretation with higher-dimensional ellipsoids and conic extrapolation
- Automatic modular abstractions for template numerical constraints
- Fast numerical program analysis with reinforcement learning
- Inferring Min and Max Invariants Using Max-Plus Polyhedra
- Automatic synthesis of \(k\)-inductive piecewise quadratic invariants for switched affine control programs
Uses Software
This page was built for publication: Abstract interpretation meets convex optimization
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q435969)
