Difference between revisions of "Pagai"
Jump to navigation
Jump to search
(Created page with "'''Pagai''' is a research prototype for static analysis by abstract interpretation, mostly implemented by [http://www-verimag.imag.fr/~jhenry Julien Henry]. It implements seve...") |
|||
| (One intermediate revision by the same user not shown) | |||
| 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 23: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.
