2 PAGAI: a path sensitive static analyzer
Julien Henry, David P. Monniaux, Matthieu Moy · arXiv (Cornell University) · 2012
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 variables of the analyzed program. PAGAI implements various state-of-the-art algorithms combining ab-stract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside the control flow graph while avoiding system-atic exponential enumerations. It is parametric in the abstract domain in use, the iteration algorithm, and the decision procedure. We compared the time and precision of various combinations of analy-sis algorithms and abstract domains, with extensive experiments both on personal benchmarks and widely available GNU programs. 1