Difference between revisions of "Pagai"

From STATOR
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.