Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case

DOI10.1007/s10703-015-0230-7zbMath1341.68031OpenAlexW250118690MaRDI QIDQ888469

Pierre-Loïc Garoche, Pierre Roux

Publication date: 30 October 2015

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

Full work available at URL: https://doi.org/10.1007/s10703-015-0230-7

zbMATH Keywords

Lyapunov functionsellipsoidsstatic analysiswideningabstract interpretationpolicy iterationscontrollersquadratic templates

Mathematics Subject Classification ID

Numerical optimization and variational techniques (65K10) Lyapunov and other classical stabilities (Lagrange, Poisson, (L^p, l^p), etc.) in control theory (93D05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

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

Uses Software

• Coq
• mctoolbox
• Aspic
• Flocq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Abstract interpretation meets convex optimization
• Acceleration of the abstract fixpoint computation in numerical program analysis
• Abstract interpretation of mobile systems
• Verification of positive definiteness
• Verification methods: Rigorous results using floating-point arithmetic
• A generic ellipsoid abstract domain for linear time invariant systems
• Static Analysis of Finite Precision Computations
• Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis
• Linear Matrix Inequalities in System and Control Theory
• Semidefinite Programming
• Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely
• Integrating Policy Iterations in Abstract Interpreters
• Systematic design of program transformation frameworks by abstract interpretation
• Abstract Interpretation Frameworks
• Programming Languages and Systems
• Programming Languages and Systems
• Hybrid Systems: Computation and Control
• Computer Aided Verification
• Computer Aided Verification
• Static Analysis by Policy Iteration on Relational Domains
• Precise Fixpoint Computation Through Strategy Iteration
• Probleme General de la Stabilite du Mouvement. (AM-17)