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...") |
|||
Line 1: | Line 1: | ||
− | '''Pagai''' is a research prototype for static analysis by abstract interpretation, mostly implemented by [http://www-verimag.imag.fr/~jhenry Julien Henry]. It implements several analysis algorithms, mixing abstract interpretation using the [[APRON]] library with [[Satisfiability_Modulo_Theories|SMT-solving]]. It takes as input [[wikipedia:LLVM|LLVM]] bitcode files. | + | '''Pagai''' is a research prototype for static analysis by abstract interpretation, mostly implemented by [http://www-verimag.imag.fr/~jhenry Julien Henry]. 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. |
Revision as of 21:47, 25 October 2012
Pagai is a research prototype for static analysis by abstract interpretation, mostly implemented by Julien Henry. 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.