Proving Termination by Policy Iteration

DOI10.1016/j.entcs.2012.09.008zbMath1294.68061OpenAlexW2027936721WikidataQ113318057 ScholiaQ113318057MaRDI QIDQ5170173

Damien Massé

Publication date: 22 July 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2012.09.008

zbMATH Keywords

policy iterationabstract interpretationtermination analysistemplate constraint matrices

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Numerical invariants through convex relaxation and max-strategy iteration

Uses Software

• Aspic

Cites Work

• The octagon abstract domain
• Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
• An abstract interpretation framework for termination
• Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis
• Precise Relational Invariants Through Strategy Iteration
• Combining Widening and Acceleration in Linear Relation Analysis
• Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely
• Abstract Interpretation Frameworks
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Precise Fixpoint Computation Through Strategy Iteration
• Deciding Conditional Termination

This page was built for publication: Proving Termination by Policy Iteration