-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
executable file
·350 lines (304 loc) · 11.9 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<!--<meta http-equiv="X-UA-Compatible" content="IE=edge"> -->
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<meta name="description" content="">
<meta name="author" content="Julien Henry">
<link rel="shortcut icon" href="../../docs-assets/ico/favicon.png">
<script src="https://code.jquery.com/jquery-1.10.2.min.js"></script>
<script src="./dist/js/bootstrap.min.js"></script>
<script src="./dist/js/holder.js"></script>
<script src="./dist/js/anchor.js"></script>
<script src="./dist/js/bootstrap-scrollspy.js"></script>
<title>Julien Henry</title>
<!-- Bootstrap core CSS -->
<link href="./dist/css/bootstrap.css" rel="stylesheet">
<link rel="stylesheet" href="./dist/font-awesome/css/font-awesome.min.css">
<!-- HTML5 shim and Respond.js IE8 support of HTML5 elements and media queries -->
<!--[if lt IE 9]>
<script src="https://oss.maxcdn.com/libs/html5shiv/3.7.0/html5shiv.js"></script>
<script src="https://oss.maxcdn.com/libs/respond.js/1.3.0/respond.min.js"></script>
<![endif]-->
<!-- Custom styles for this template -->
<link href="carousel.css" rel="stylesheet">
<script src="https://google-code-prettify.googlecode.com/svn/loader/run_prettify.js"></script>
</head>
<!-- NAVBAR
================================================== -->
<body data-spy="scroll" data-target=".navbar">
<div id="home" class="navbar-wrapper">
<div class="container">
<div class="navbar navbar-inverse navbar-fixed-top" role="navigation">
<div class="container">
<div class="navbar-header">
<a href="#home" class="navbar-brand anchorLink">J. Henry</a>
</div>
<div class="navbar-collapse collapse">
<ul class="nav navbar-nav">
<li class="active"><a href="#home" class="anchorLink">Home</a></li>
<li><a href="#research" class="anchorLink">Research</a></li>
<li><a href="#teaching" class="anchorLink">Teaching</a></li>
<li><a href="#misc" class="anchorLink">Misc.</a></li>
</ul>
</div>
</div>
</div>
</div>
</div>
<!-- Carousel
================================================== -->
<div class="mycarousel slide" data-ride="mycarousel">
<div class="mycarousel-inner">
<div class="item active">
<div class="container">
<div class="mycarousel-caption">
<div class="col-sm-6 photo">
<img src="photo2.png" height="250" alt="me" />
</div>
<div class="col-sm-6">
<h1 class="text-left">Julien Henry</h1>
<h2 class="text-left">Senior Developer at Mathworks</h2>
<h2 class="text-left">Expert in Static Program Analysis</h2>
<br/>
<br/>
<ul class="followme">
<li>
<a href="mailto:[email protected]">
<i class="fa fa-envelope"></i>Email
</a>
</li>
<li>
<a
href="http://scholar.google.fr/citations?user=uHRSM-EAAAAJ"><i
class="fa fa-external-link"></i>Google Scholar</a>
</li>
<li>
<a href="http://dblp.uni-trier.de/pers/hd/h/Henry:Julien.html">
<i class="fa fa-search"></i>DBLP
</a>
</li>
<li>
<a href="http://fr.linkedin.com/in/julienhenry/">
<i class="fa fa-linkedin"></i>LinkedIn
</a>
</li>
</ul>
</div>
</div>
</div>
</div>
</div>
</div><!-- /.mycarousel -->
<!-- Marketing messaging and featurettes
================================================== -->
<!-- Wrap the rest of the page in another container to center all the content. -->
<div class="container marketing">
<!-- Three columns of text below the mycarousel -->
<div class="row">
<div class="col-lg-4">
<h2>About</h2>
<p class="text-left">
I am currently a senior developer at Mathworks, where I work on the Polyspace products.
</p>
<p class="text-left">
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 <a href="http://pages.cs.wisc.edu/~reps">Thomas Reps</a>.
</p>
<p class="text-left">
I completed a PhD in Computer Science in the Synchrone team of the Verimag laboratory, advised by Dr.
<a href="http://www-verimag.imag.fr/~monniaux">David Monniaux</a> and
Dr. <a href="http://www-verimag.imag.fr/~moy">Matthieu Moy</a>.
</p>
<p class="text-left">
The title of my PhD is "Static Analysis by Abstract Interpretation and Decision Procedures".
</p>
<p class="text-left">
<b>Email:</b> julienhenry23 AT gmail DOT com
</p>
</div><!-- /.col-lg-4 -->
<div class="col-lg-4">
<h2>Research</h2>
<p class="text-left">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.
</p>
<p><a class="btn btn-default anchorLink" href="#research" role="button">More »</a></p>
</div><!-- /.col-lg-4 -->
<div class="col-lg-4">
<h2>Teaching</h2>
<p class="text-left">
From september 2011 to January 2014, I was teaching assistant at Grenoble-INP Ensimag.
</p>
<p class="text-left">
From september 2012 to January 2014, I was also teaching at Grenoble-INP
Esisar.
</p>
<p class="text-left"><a class="btn btn-default anchorLink" href="#teaching" role="button">More »</a></p>
</div><!-- /.col-lg-4 -->
</div><!-- /.row -->
<!-- START THE FEATURETTES -->
<hr class="featurette-divider">
<div class="row featurette" id="research">
<div class="col-md-7">
<h2 class="featurette-heading">Research</h2>
<h3>PhD Thesis</h3>
Julien Henry <B>Static Analysis by Abstract Interpretation and Decision Procedures</B><br>
<a href="./pdf/thesis-JulienHenry.pdf"><i class="fa fa-download pad"></i>Manuscript</a>, <a href="./pdf/defense-JulienHenry.pdf"><i class="fa fa-download pad"></i>slides</a>
<h3>Publications</h3>
<ul>
<li>Julien Henry, Mihail Asavoae, David Monniaux, Claire Maiza:
<B>How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics</B>,
(<a href="http://www.ittc.ku.edu/lctes14/">LCTES'14</a>), <a
href="./pdf/LCTES14.pdf"><i class="fa fa-download pad"></i>paper</a>, <a href="./pdf/LCTES14-slides.pdf"><i class="fa fa-download pad"></i>slides</a>
</li>
<li>Julien Henry, David Monniaux, Matthieu Moy:
<B>PAGAI: a path sensitive static analyser </B>,
(<a href="http://tapas2012.inrialpes.fr/">TAPAS'12</a>), <a href="./pdf/TAPAS12.pdf"><i class="fa fa-download pad"></i>paper</a>, <a href="./pdf/TAPAS12-slides.pdf"><i class="fa fa-download pad"></i>slides</a>
</li>
<li>Julien Henry, David Monniaux, Matthieu Moy:
<B>Succinct Representations for Abstract Interpretation</B>, Static Analysis Symposium 2012
(<a href="http://www.sas2012.ens.fr/index.html">SAS'12</a>), pages 283-299,
<a href="./pdf/SAS12.pdf"><i class="fa fa-download pad"></i>paper</a>,
<a href="./pdf/SAS12-slides.pdf"><i class="fa fa-download pad"></i>slides</a>
</li>
<li>Nicolas Halbwachs, Julien Henry:
<B>When the decreasing sequence fails</B>, Static Analysis Symposium 2012
(<a href="http://www.sas2012.ens.fr/index.html">SAS'12</a>),
pages 198-213,
<a href="./pdf/SAS12b.pdf"><i class="fa fa-download pad"></i>paper</a>
</li>
</ul>
<h3>Pagai static analyser</h3>
<p>
I am the main contributor of
<a href="http://pagai.forge.imag.fr">Pagai</a>, 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.
</p>
<p><a class="btn btn-lg btn-success" href="http://pagai.forge.imag.fr"
role="button">Download Pagai »</a></p>
<ul>
<li><a href="./svcomp/Loop.html">SV-Comp Loop</a></li>
<li><a href="./svcomp/ProductLines.html">SV-Comp ProductLines</a></li>
<li><a href="./svcomp/ControlFlowInteger.html">SV-Comp ControlFrowInteger</a></li>
</ul>
<h3>LCTES'14 SMT-lib2 benchmarks</h3>
<p>Some benchmarks are available <a href="https://forge.imag.fr/frs/download.php/578/LCTES-smtlib2-benchmarks.tar.gz">here</a>.</p>
</div>
<div class="col-md-5">
<pre class="prettyprint"><code>~$ 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 */
}
</code></pre>
</div>
</div>
<hr class="featurette-divider">
<div class="row featurette" id="teaching">
<div class="col-md-5">
<!--
<img class="featurette-image img-responsive" data-src="holder.js/500x500/auto" alt="Generic placeholder image">
-->
</div>
<div class="col-md-7">
<h2 class="featurette-heading">Teaching <span class="text-muted"> (in
French...)</span></h2>
<h4>Langages et Compilation</h4>
<p><a class="btn btn-default anchorLink" href="./teaching/cs410.html" role="button">More »</a>
</p>
<p>
CM et TD, 4A Grenoble-INP Esisar, 2012-2013 à 2013-2014
</p>
<h4>Circuits Numériques et Éléments d'Architecture</h4>
<p>
TP, 1A Grenoble-INP Ensimag, de 2011-2012 à 2013-2014
</p>
<h4>TP Unix : Intro et Programmation shell</h4>
TP, 1A Grenoble-INP Ensimag, 2013-2014
<h4>Projet Bases de Données</h4>
<p>
TP, 2A Grenoble-INP Ensimag, 2011-2012
</p>
<h4>Principes des Systèmes de Gestion de Bases de Données</h4>
<p>
Cours-TD, 2A Grenoble-INP Ensimag, 2011-2012
</p>
</div>
</div>
<hr class="featurette-divider">
<div class="row featurette" id="misc">
<div class="col-md-7">
<h2 class="featurette-heading">Misc. <span class="text-muted">External
links and lecture notes</span></h2>
<p class="lead">
I provide some lecture notes (in French), that I wrote as an
Esimag student.
</p>
<p>
<a href="../pdf/TL.pdf">
<i class="fa fa-book pad"></i>
Théorie des langages, Ensimag 1A
</a>
</p>
<p>
<a href="../pdf/TL2.pdf">
<i class="fa fa-book pad"></i>
Calculabilité, Ensimag 1A
</a>
</p>
<p>
<a href="../pdf/analyse.pdf">
<i class="fa fa-book pad"></i>
Analyse pour l'ingénieur, Ensimag 1A
</a>
</p>
<p>
<a href="../pdf/Algo4.pdf">
<i class="fa fa-book pad"></i>
Algorithmique Avancée, Ensimag 2A
</a>
</p>
<p class="lead">
Here are some useful LaTeX memos (in French):
</p>
<ul>
<li><a href="http://tex.loria.fr/general/aide-memoire-latex-seguin1998.pdf">Aide mémoire de Vincent Seguin</a></li>
<li><a href="http://gwendal.haudebourg.free.fr/maths/pdf/aide_memoire.pdf">gwendal.haudebourg.free.fr</a></li>
<li><a href="ftp://ftp.laas.fr/pub/Logiciels/latex/flshort/flshort-3.20.pdf">Une courte (?) introduction à LaTeX 2e</a></li>
<li><a href="ftp://ftp.inria.fr/pub/TeX/CTAN/info/JMPL.ps.gz">Joli Manuel Pour LaTeX</a></li>
</ul>
</div>
</div>
<hr class="featurette-divider">
<!-- /END THE FEATURETTES -->
<!-- FOOTER -->
<footer>
</footer>
</div><!-- /.container -->
</body>
</html>