Precise Relational Invariants Through Strategy Iteration

DOI10.1007/978-3-540-74915-8_6MaRDI QIDQ3608402zbMATH OpenOpenAlexFDO

Authors Thomas Martin Gawlitza, Helmut Seidl

Publication date 5 March 2009

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-74915-8_6

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Special problems of linear programming (transportation, multi-index, data envelopment analysis, etc.) (90C08)

Recommendations

• Precise Fixpoint Computation Through Strategy Iteration
• Static Analysis by Policy Iteration on Relational Domains
• Computing relaxed abstract semantics w.r.t. quadratic zones precisely
• Invariant generation through strategy iteration in succinctly represented control flow graphs
• Improving strategies via SMT solving

Cited in

(12)

• Numerical invariants through convex relaxation and max-strategy iteration
• Static analysis by abstract interpretation: a mathematical programming approach
• Template-based unbounded time verification of affine hybrid automata
• Improving strategies via SMT solving
• Invariant generation through strategy iteration in succinctly represented control flow graphs
• Abstract interpretation meets convex optimization
• Tropical linear-fractional programming and parametric mean payoff games
• Computing relaxed abstract semantics w.r.t. quadratic zones precisely
• Proving termination by policy iteration
• Static Analysis by Policy Iteration on Relational Domains
• Precise Fixpoint Computation Through Strategy Iteration
• On the Monniaux problem in abstract interpretation

Describes a project that uses

Uses Software

• Octagon

This page was built for publication: Precise Relational Invariants Through Strategy Iteration

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