Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs

DOI10.2168/LMCS-8(3:29)2012zbMath1248.68142arXiv1209.0643MaRDI QIDQ3166219

Thomas Martin Gawlitza, David Monniaux

Publication date: 22 October 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1209.0643

zbMATH Keywords

abstract interpretationstatic program analysisSMT solvingstrategy improvement algorithmsfixpoint equation systems

Mathematics Subject Classification ID

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

Related Items (4)

Descending chains and narrowing on template abstract domains ⋮ On the decidability of the existence of polyhedral invariants in transition systems ⋮ Narrowing Operators on Template Abstract Domains ⋮ A Survey of Satisfiability Modulo Theory

Uses Software

• SMT-LIB
• Yices
• Aspic
• Octagon
• ASTREE

This page was built for publication: Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs