Difference between revisions of "Pagai"
Jump to navigation
Jump to search
| Line 1: | Line 1: | ||
| − | '''Pagai''' is a research prototype for static analysis by abstract interpretation | + | '''Pagai''' is a research prototype for static analysis by abstract interpretation. |
| + | |||
| + | It is developed [http://www-verimag.imag.fr/~jhenry Julien Henry], with contributions by [[User:David Monniaux|David Monniaux]], [http://www-verimag.imag.fr/~moy/ Matthieu Moy] and Rahul Nanda. | ||
| + | |||
| + | It implements several analysis algorithms, mixing abstract interpretation using the [[APRON]] library with [[wikipedia:Satisfiability_Modulo_Theories|SMT-solving]]. It takes as input [[wikipedia:LLVM|LLVM]] bitcode files. | ||
The [https://forge.imag.fr/projects/pagai/ source code] of the tool is available. | The [https://forge.imag.fr/projects/pagai/ source code] of the tool is available. | ||
Latest revision as of 22:02, 25 October 2012
Pagai is a research prototype for static analysis by abstract interpretation.
It is developed Julien Henry, with contributions by David Monniaux, Matthieu Moy and Rahul Nanda.
It implements several analysis algorithms, mixing abstract interpretation using the APRON library with SMT-solving. It takes as input LLVM bitcode files.
The source code of the tool is available.
