PAGAI: A path sensitive static analyser

Citations of this article
Mendeley users who have this article in their library.


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 abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside the control flow graph while avoiding systematic 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 analysis algorithms and abstract domains, with extensive experiments both on personal benchmarks and widely available GNU programs. © 2012 Elsevier B.V. All rights reserved.




Henry, J., Monniaux, D., & Moy, M. (2012). PAGAI: A path sensitive static analyser. In Electronic Notes in Theoretical Computer Science (Vol. 289, pp. 15–25).

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free