Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs

We consider the problem of computing numerical invariants of programs, for instance bounds on the values of numerical program variables. More specifically, we study the problem of performing static analysis by abstract interpretation using template linear constraint domains. Such invariants can be o...

Full description

Bibliographic Details
Main Authors: Thomas Martin Gawlitza, David Monniaux
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2012-09-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/689/pdf