Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis
From MaRDI portal
Publication:3558213
DOI10.1007/978-3-642-11957-6_3zbMath1260.68082OpenAlexW1896502719MaRDI QIDQ3558213
Assalé Adjé, Eric Goubault, Stéphane Gaubert
Publication date: 4 May 2010
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-11957-6_3
Related Items (15)
Donut Domains: Efficient Non-convex Domains for Abstract Interpretation ⋮ Template-Based Unbounded Time Verification of Affine Hybrid Automata ⋮ A sums-of-squares extension of policy iterations ⋮ Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case ⋮ Abstract interpretation meets convex optimization ⋮ Tropical linear-fractional programming and parametric mean payoff games ⋮ Generalizing the Template Polyhedral Domain ⋮ Improving Strategies via SMT Solving ⋮ Counterexample- and simulation-guided floating-point loop invariant synthesis ⋮ Numerical invariants through convex relaxation and max-strategy iteration ⋮ Proving Termination by Policy Iteration ⋮ Validating numerical semidefinite programming solvers for polynomial invariants ⋮ A zonotopic framework for functional abstractions ⋮ Policy iteration in finite templates domain ⋮ Static Analysis by Abstract Interpretation: A Mathematical Programming Approach
Uses Software
This page was built for publication: Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis
