Integrating Policy Iterations in Abstract Interpreters

DOI10.1007/978-3-319-02444-8_18MaRDI QIDQ5166691zbMATH OpenOpenAlexFDO

Authors Pierre Roux, Pierre-Loïc Garoche

Publication date 8 July 2014

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-02444-8_18

zbMATH Keywords

abstract interpretationellipsoidslinear systems with guardspolicy iterationquadratic invariantssemidefinite programming

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Semidefinite programming (90C22)

Recommendations

• Policy iteration within logico-numerical abstract domains
• A state space distribution policy based on abstract interpretation
• Policy iteration for bounded-parameter POMDPs
• Policy iteration in finite templates domain
• Formal Policy Synthesis for Continuous-State Systems via Reinforcement Learning
• Program analysis with local policy iteration
• Abstract interpretation of programs as Markov decision processes

Cited in

(11)

• Counterexample- and simulation-guided floating-point loop invariant synthesis
• Template polyhedra and bilinear optimization
• A sums-of-squares extension of policy iterations
• Program analysis with local policy iteration
• Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
• Policy iteration within logico-numerical abstract domains
• Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
• Automatic synthesis of piecewise linear quadratic invariants for programs
• Coupling policy iterations with piecewise quadratic Lyapunov functions
• Automatic synthesis of k-inductive piecewise quadratic invariants for switched affine control programs
• Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case

Describes a project that uses

Uses Software

• Octagon

This page was built for publication: Integrating Policy Iterations in Abstract Interpreters

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