328 citations · 732 across the 43 of their papers we have counts for
3 papers · 1 filter
Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs
Thomas Martin Gawlitza, David Monniaux
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…
PAGAI: a path sensitive static analyzer
Julien Henry, David Monniaux, Matthieu Moy
We describe the design and the implementation of PAGAI, a new static analyzer working over the LLVM compiler infrastructure, which computes inductive invariants on the numerical va…
Succinct Representations for Abstract Interpretation
Julien Henry, David Monniaux, Matthieu Moy
Abstract interpretation techniques can be made more precise by distinguishing paths inside loops, at the expense of possibly exponential complexity. SMT-solving techniques and spar…