I am currently a senior developer at Mathworks, where I work on the Polyspace products.
Previously, I was a senior scientist at GrammaTech, Inc, in Madison, WI, USA. Before that, I was a postdoctoral researcher at the University of Wisconsin Madison, under the direction of Professor Thomas Reps.
I completed a PhD in Computer Science in the Synchrone team of the Verimag laboratory, advised by Dr. David Monniaux and Dr. Matthieu Moy.
The title of my PhD is "Static Analysis by Abstract Interpretation and Decision Procedures".
Email: julienhenry23 AT gmail DOT com
I am interested in static analysis by Abstract Interpretation, which is a commonly used techique to discover properties about a program (loop invariants, etc.). This technique computes an over-approximations of the set of possible states of the program. I am particularly interested in the relation between abstract interpretation and decision procedures (Satisfiability Modulo Theories); in particular: how to improve abstract interpretation using SMT, and how to improve the efficiency of SMT solvers by using techniques used in abstract interpretation.
From september 2011 to January 2014, I was teaching assistant at Grenoble-INP Ensimag.
From september 2012 to January 2014, I was also teaching at Grenoble-INP Esisar.
I am the main contributor of Pagai, an open source static analyser for LLVM bitcode. It computes invariants involving the numerical variables of a program using state-of-the-art Abstract Interpretation based techniques.
Some benchmarks are available here.
~$ pagai -i main.bc
int main() {
int x = 0;
int y = 0;
/* reachable */
while (1) {
/* invariant:
102-x-y >= 0
y >= 0
x-y >= 0
*/
if (x <= 50) {
// safe
y++;
} else // safe
y--;
if (y < 0) break;
// safe
x++;
}
// safe
/* assert OK */
assert(x+y<=101);
/* assert OK */
assert(x <= 102);
/* reachable */
}
CM et TD, 4A Grenoble-INP Esisar, 2012-2013 à 2013-2014
TP, 1A Grenoble-INP Ensimag, de 2011-2012 à 2013-2014
TP, 2A Grenoble-INP Ensimag, 2011-2012
Cours-TD, 2A Grenoble-INP Ensimag, 2011-2012
I provide some lecture notes (in French), that I wrote as an Esimag student.
Théorie des langages, Ensimag 1A
Analyse pour l'ingénieur, Ensimag 1A
Algorithmique Avancée, Ensimag 2A
Here are some useful LaTeX memos (in French):