-
Notifications
You must be signed in to change notification settings - Fork 9
Expand file tree
/
Copy pathindex.html
More file actions
365 lines (338 loc) · 21.2 KB
/
index.html
File metadata and controls
365 lines (338 loc) · 21.2 KB
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
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
<!DOCTYPE html>
<html>
<head>
<meta charset="utf-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1">
<meta name="author" content="Damien Zufferey" />
<meta name="language" content="en" />
<meta property="og:title" content="Damien Zufferey" />
<meta property="og:type" content="website" />
<meta property="og:url" content="https://dzufferey.github.io/" />
<meta property="og:image" content="https://dzufferey.github.io/files/me4.png" />
<meta property="og:description" content="Damien Zufferey's home page." />
<!-- style -->
<link rel="stylesheet" href="lib/bootstrap/css/bootstrap.min.css" type="text/css" />
<link rel="stylesheet" href="lib/style.css" type="text/css" />
<title>Damien Zufferey</title>
</head>
<body>
<nav class="navbar">
<div class="container bigger120">
<div class="navbar-header">
<button type="button" class="navbar-toggle" data-toggle="collapse" data-target="#myNavbar">
<span class="icon-bar"></span>
<span class="icon-bar"></span>
<span class="icon-bar"></span>
</button>
<a class="navbar-brand" href="#"><big class="my-name">Damien Zufferey</big></a>
</div>
<div class="collapse navbar-collapse" id="myNavbar">
<ul class="nav navbar-nav">
<!--li><a href="#sec-bio">Bio</a></li-->
<!--li><a href="#sec-consulting">Consulting</a></li-->
<li><a href="#sec-pub">Publications</a></li>
<li><a href="#sec-proj">Research</a></li>
<li><a href="#sec-prof">Professional Activities</a></li>
<li><a href="#sec-misc">Misc.</a></li>
</ul>
<ul class="nav navbar-nav navbar-right">
<!--li><a href="http://www.csail.mit.edu/">MIT CSAIL</a></li-->
</ul>
</div>
</div>
</nav>
<!-- Short Bio -->
<div class="container" id="sec-bio">
<div class="row">
<div class="col-sm-3">
<img src="files/me4.png" alt="Damien Zufferey" class="center-block img-responsive">
</div>
<div class="col-sm-6">
<p>
I'm a computer scientist specialized in the areas of
<ul>
<li>program analysis and verification,</li>
<li>programming languages and session types,</li>
<li>distributed, embedded, and cyber-physical systems.</li>
</ul>
I focus on developing programming abstractions designed that are amenable to automated verification, i.e., the automatic analysis of software to find mathematical proofs showing the code meets its specification.
</p>
<p>
I'm currently working as a static analysis scientist at <a href="https://www.sonarsource.com/">Sonar Source</a>.
In 2022, I worked for <a href="https://www.signaloid.ai/">Signaloid</a>; first as a consultant, and then as Quality Assurance Lead.
Between 2016 and 2021, I was a research group leader at <a href="https://www.mpi-sws.org/">MPI-SWS</a>.
Until September 2016, I was a Postdoctoral Associate at <a href="https://www.csail.mit.edu/">MIT CSAIL</a> in <a href="http://people.csail.mit.edu/rinard/">Martin Rinard</a>'s group.
I received my PhD in 2013, working under supervision of <a href="http://www.ist.ac.at/research/research-groups/henzinger-group/">Thomas A. Henzinger</a>
at the <a href="https://ist.ac.at/">Institute of Science and Technology Austria (IST Austria)</a>.
Prior to that I received a Master in computer science from <a href="https://www.epfl.ch/">EPFL</a> in 2009.
</p>
</div>
<div class="col-sm-3">
<!--
<img src="files/logo.png" alt="Damien Zufferey" class="center-block img-responsive">
-->
<!--p>
<strong>Address</strong><br>
Max Planck Institute for Software Systems<br>
Paul-Ehrlich-Str. 26<br>
67663 Kaiserslautern<br>
Germany
</p-->
<p>
<strong>E-Mail</strong><br>
<script type="text/javascript" language="javascript">
<!--
// Email obfuscator script 2.1 by Tim Williams, University of Arizona
// Random encryption key feature by Andrew Moulden, Site Engineering Ltd
// This code is freeware provided these four comment lines remain intact
// A wizard to generate this code is at http://www.justudin.com/anti-spam-email/
{ coded = "iMAqNV.CvIINGNk@MmvAVq.NbIm.Xs"
key = "opV1IQPmrRg7TNhxM0F3SukOBzKc8iZbtUnDfAGl9Jw5seWEaj2v6LyC4XYqHd"
shift=coded.length
link=""
for (i=0; i<coded.length; i++) {
if (key.indexOf(coded.charAt(i))==-1) {
ltr = coded.charAt(i)
link += (ltr)
}
else {
ltr = (key.indexOf(coded.charAt(i))-shift+key.length) % key.length
link += (key.charAt(ltr))
}
}
document.write("<a href='mailto:"+link+"'>"+link+"</a>")
}
//-->
</script><noscript>
<img src="files/email.svg" alt="email" width="50%" class="img-responsive">
</noscript>
</p>
<p>
<strong>CV</strong>
<ul>
<li><a href="files/damien_cv_short.pdf">Short CV</a></li>
<li><a href="files/damien_cv.pdf">Academic CV</a></li>
</ul>
</p>
</div>
</div>
</div>
<div class="container separation"></div>
<!--div class="container" id="sec-consulting">
<h2>Consulting</h2>
<p>
I offer consulting in my specialization area (see above).
In particular, if you are developing safety-critical software and you are interested in using formal methods (model checking, theorem proving, etc.) I can help you.
To get a better idea of what I can do, check my publication record below.
</p>
<p>
If something looks interesting to you, just send me an email to discuss your needs and what I can bring to that table.
</p>
</div-->
<div class="container" id="sec-pub">
<ul class="nav nav-tabs">
<li class="navbar-text"><h2>Publications:</h2></li>
<li class="active"><a data-toggle="tab" href="#pub-recent"><h2>Recent</h2></a></li>
<li> <a data-toggle="tab" href="#pub-all"> <h2>All</h2></a></li>
</ul>
<div class="tab-content">
<div class="tab-pane fade in active" id="pub-recent">
<div class="progress">
<div class="progress-bar progress-bar-striped active" role="progressbar" aria-valuenow="100" aria-valuemin="0" aria-valuemax="100" style="width:100%">
Loading recent publications ...
</div>
</div>
<a class="hidden" href="recent.json"></a>
</div>
<div class="tab-pane fade" id="pub-all">
<div class="progress">
<div class="progress-bar progress-bar-striped active" role="progressbar" aria-valuenow="100" aria-valuemin="0" aria-valuemax="100" style="width:100%">
Loading all publications ...
</div>
</div>
<a class="hidden" href="publications.json"></a>
</div>
</div>
<p>
<a href="https://scholar.google.de/citations?user=DM1nCKsAAAAJ">Google Scholar</a> has citation metrics for my publications.
The publications are in <a href="http://www.ams.org/profession/leaders/CultureStatement04.pdf">alphabetical order</a> except when there is a large difference of contribution.
</p>
</div>
<div class="container separation"></div>
<div class="container" id="sec-proj">
<ul class="nav nav-tabs">
<li class="navbar-text"><h2>Research:</h2></li>
<li class="active"><a data-toggle="tab" href="#research-project"><h2>Projects</h2></a></li>
<li> <a data-toggle="tab" href="#research-group"><h2>Group</h2></a></li>
<li> <a data-toggle="tab" href="#research-tools"><h2>Tools</h2></a></li>
</ul>
<div class="tab-content">
<div id="research-project" class="tab-pane fade in active">
<div class="list-group">
<a href="https://github.com/MPI-SWS/pgcd/" class="list-group-item">
<h4 class="list-group-item-heading">Design, programming, and verification of robotic system</h4>
<p class="list-group-item-text">
Robotics applications involve programming concurrent components synchronising through messages while simultaneously executing motion primitives that control the state of the physical world.
These applications are typically programmed in low-level imperative programming languages which provide little support for abstraction or reasoning.
We are looking at a programming model which brings together software and hardware.
This project has multiple parts.
With PGCD we are working on an unifying programming model combining message-passing concurrency and control code which interacts with the physical world.
With MPerl we look at how progress in rapid manufacturing tools like 3D printers influence the way we write code for robotic systems.
More precisely, we are working generating control code from parametric description of robotic designs.
</p>
</a>
<a href="https://github.com/dzufferey/psync" class="list-group-item">
<h4 class="list-group-item-heading">Programming abstraction and verification of fault tolerant distributed algorithms (PSync)</h4>
<p class="list-group-item-text">
Fault-tolerant distributed systems play an important role in many critical applications.
However, concurrency, uncertain message delays, and the occurrence of faults make those systems hard to design, implement, and verify.
PSync is a framework for writing and verifying high-level implementations of fault-tolerant distributed algorithms.
PSync is based on the Heard-Of model and provides communication-closed rounds as primitive, which both simplifies the implementation of the fault-tolerant systems, and makes them more amenable to automated verification.
</p>
</a>
<a href="https://cs.nyu.edu/wies/software/grasshopper/" class="list-group-item">
<h4 class="list-group-item-heading">Verification of heap-manipulating programs (GRASShopper)</h4>
<p class="list-group-item-text">
GRASShopper is an experimental verification tool for programs that manipulate dynamically allocated data structures.
GRASShopper programs can be annotated with specifications expressed in a decidable specification logic to check functional correctness properties.
The logic supports mixing of separation logic and first-order logic assertions, yielding expressive yet concise specifications.
</p>
</a>
</div>
</div>
<div id="research-group" class="tab-pane fade">
<h3>PhD Students</h3>
<ul>
<li><a href="https://people.mpi-sws.org/~mpirron/">Marcus Pirron</a></li>
<li><a href="https://people.mpi-sws.org/~mathur/">Aman Shankar Mathur</a> (co-advised with Rupak Majumdar)</li>
<li><a href="https://www.mpi-sws.org/people/fstutz/">Felix Stutz</a></li>
</ul>
</div>
<div id="research-tools" class="tab-pane fade">
<p>
A list of the various tools that I developed and participated in the development.
Most of these tools are academic prototypes and are not maintained anymore.
</p>
<ul>
<li><a href="https://github.com/MPI-SWS/pgcd/">PGCD</a>: a programming and verification tool for robotic systems with an emphasis on coordination of multiple robots.</li>
<li><a href="https://gitlab.mpi-sws.org/mpirron/mperl">MPerl</a>: automating the generation of control code for robotic manipulators.</li>
<li><a href="https://github.com/dzufferey/psync">PSync</a>: DSL for fault-tolerant distributed algorithms using partially-synchronous communication-closed rounds.</li>
<li><a href="https://cs.nyu.edu/wies/software/grasshopper/">GRASShopper</a>: a verification tool that checks separation logic specifications of heap manipulating programs.</li>
<li><a href="./picasso/">Picasso</a>: a PI-CAlculuS-based SOftware analyzer.</li>
<li><a href="http://pub.ist.ac.at/automata_tutor/">Automata Tutor</a>: a website for teaching automata theory to undergraduate students. Later the project was taken over by groups at UPenn and UIUC and became <a href="http://www.automatatutor.com/">http://www.automatatutor.com/</a></li>
<li><a href="http://pub.ist.ac.at/~cernyp/colt/">CoLT</a>: Concurrency using Lockstep Tool, a tool for model checking of linearizability of concurrent data structure implementations.</li>
<li><a href="https://github.com/dzufferey/csisat/">CSIsat</a>: Constraint Solving for Interpolation, a tool to compute Craig interpolant in QF LA+EUF.</li>
<li><a href="http://mtc.epfl.ch/software-tools/blast/">Blast</a>: Berkeley Lazy Abstraction Software Verification Tool.</li>
</ul>
</div>
</div>
</div>
<div class="container separation"></div>
<div class="container" id="sec-prof">
<ul class="nav nav-tabs">
<li class="navbar-text"><h2>Professional Activities:</h2></li>
<li class="active"><a data-toggle="tab" href="#prof-pc"><h2>Program Committee</h2></a></li>
<li><a data-toggle="tab" href="#prof-rev"><h2>Reviewing</h2></a></li>
<li><a data-toggle="tab" href="#prof-teach"><h2>Teaching</h2></a></li>
</ul>
<div class="tab-content">
<div id="prof-pc" class="tab-pane fade in active">
<h3>PC co-chair</h3>
<ul>
<li><a href="https://popl20.sigplan.org/home/VMCAI-2020">VMCAI 2020</a>, 21st International Conference on Verification, Model Checking, and Abstract Interpretation.</li>
<li><a href="http://nsv19.mpi-sws.org/">NSV 19</a>, 12th International Workshop on Numerical Software Verification.</li>
<li><a href="http://cavconference.org/2017/verification-mentoring-workshop/">VMW 2017</a>, Verification Mentoring Workshop 2017.</li>
</ul>
<h3>PC member</h3>
<ul>
<li><a href="https://popl21.sigplan.org/">POPL 2021</a>, 48th ACM SIGPLAN Symposium on Principles of Programming Languages.</li>
<li><a href="https://etaps.org/2021/esop">ESOP 2021</a>, 30th European Symposium on Programming.</li>
<li><a href="https://sri-csl.github.io/VSTTE20/">VSTTE 2020</a>, 12th Working Conference on Verified Software: Theories, Tools, and Experiments.</li>
<li><a href="https://conf.researchr.org/home/aplas-2019">APLAS 2019</a>, 17th Asian Symposium on Programming Languages and Systems.</li>
<li><a href="https://synasc.ro/2019/">SYNASC 2019</a>, 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing.</li>
<li><a href="https://popl19.sigplan.org/track/VMCAI-2019">VMCAI 2019</a>, 20th International Conference on Verification, Model Checking, and Abstract Interpretation.</li>
<li><a href="https://conf.researchr.org/track/Scala-2018/scala-2018-papers">Scala 2018</a>, 9th ACM SIGPLAN Symposium on Scala.</li>
<li><a href="http://staticanalysis.org/sas2018/sas2018.html">SAS 2018</a>, 25th Static Analysis Symposium.</li>
<li><a href="http://cavconference.org/2018/">CAV 2018</a>, 30th International Conference on Computer-Aided Verification.</li>
<li><a href="http://vstte18.it.uu.se/">VSTTE 2018</a>, 10th Working Conference on Verified Software: Theories, Tools, and Experiments.</li>
<li><a href="https://pldi18.sigplan.org/committee/pldi-2018-src-committee">PLDI SRC 2018</a>, Student Research Competition at PLDI 2018.</li>
<li><a href="https://www.etaps.org/index.php/2018/tacas">TACAS 2018</a>, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.</li>
<li><a href="http://cavconference.org/2017/">CAV 2017</a>, 29th International Conference on Computer-Aided Verification.</li>
<li><a href="https://cs.nyu.edu/acsys/tapas2017/">TAPAS 2017</a>, 8th Workshop on Tools for Automatic Program Analysis.</li>
<li><a href="http://memocode.irisa.fr/2017">MEMOCODE 2017</a>, 15th International Conference on Formal Methods and Models for System Design.</li>
<li><a href="https://www.react.uni-saarland.de/synt2017/">SYNT 2017</a>, 6th Workshop on Synthesis.</li>
<li><a href="http://smt-workshop.cs.uiowa.edu/2016/">SMT 2016</a>, 14th International Workshop on Satisfiability Modulo Theories.</li>
<li><a href="http://gandalf2016.dmi.unict.it/">GANDALF 2016</a>, 7th International Symposium on Games, Automata, Logics and Formal Verification.</li>
<li><a href="http://formal.epfl.ch/synt/2016/">SYNT 2016</a>, 5th Workshop on Synthesis.</li>
<li><a href="http://conf.researchr.org/home/agere2015">AGERE 2015</a>, ACM SIGPLAN Workshop on Programming based on Actors, Agents, and Decentralized Control 2015.
<li><a href="http://lampwww.epfl.ch/~hmiller/scala2015/">Scala 2015</a>, Scala Symposium 2015.
<li><a href="http://lampwww.epfl.ch/~hmiller/scala2014/">Scala 2014</a>, annual Scala Workshop.
</ul>
</div>
<div id="prof-rev" class="tab-pane fade">
<p></p>
<ul>
<!--li><a href="#">LMCS</a></li-->
<li><a href="https://popl22.sigplan.org/home/VMCAI-2022">VMCAI 2022</a></li>
<li><a href="https://dl.acm.org/journal/toplas">TOPLAS 2021</a></li>
<li><a href="https://www.iros2019.org/">IROS 2019</a></li>
<li><a href="https://ieee-ceda.org/publication/ieee-transactions-computer-aided-design-integrated-circuits-systems-tcad">IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 2019</a></li>
<li><a href="https://www.concur2017.tu-berlin.de/">CONCUR 2017</a></li>
<li><a href="http://conf.researchr.org/home/POPL-2017">POPL 2017</a>, member of the External Research Committee</li>
<li><a href="http://www.uc.pt/en/congressos/ijcar2016">IJCAR 2016</a></li>
<li><a href="http://www.etaps.org/index.php/2016/fossacs">FoSSaCS 2016</a></li>
<li><a href="http://www.etaps.org/index.php/2016/fase">FASE 2016</a></li>
<li><a href="http://conference.mi.fu-berlin.de/cade-25/home">CADE 2015</a></li>
<li><a href="http://www.etaps.org/index.php/2015/tacas">TACAS 2015</a></li>
<li><a href="http://research.microsoft.com/en-us/events/vmcai2015/">VMCAI 2015</a></li>
<li><a href="http://www.sofsem.cz/sofsem15/">SOFSEM 2015</a></li>
<li><a href="#">JAR, special issue on interpolation 2014</a></li>
<li><a href="http://soft.vub.ac.be/AGERE14/">AGERE 2014</a></li>
<li><a href="http://popl.mpi-sws.org/2014/">POPL 2014</a></li>
<li><a href="http://lics.rwth-aachen.de/csl-lics14/">CSL-LICS 2014</a></li>
<li><a href="http://link.springer.com/journal/236">Acta Informatica (Volume 52)</a></li>
<li><a href="http://popl.mpi-sws.org/2013/">POPL 2013</a></li>
<li><a href="http://esec-fse.inf.ethz.ch/">ESEC/FSE 2013</a></li>
<li><a href="http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6597031">TASE 2013</a></li>
<li><a href="https://sites.google.com/site/vstte2012/call-for-papers">VSTTE 2012</a></li>
<li><a href="http://fm2012.cnam.fr/">FM 2012</a></li>
<li><a href="http://conferences.ncl.ac.uk/concur-2012/">CONCUR 2012</a></li>
<li><a href="http://www.etaps.org/index.php/2011/fossacs">FoSSaCS 2011</a></li>
</ul>
</div>
<div id="prof-teach" class="tab-pane fade">
<p></p>
<ul>
<li><a href="https://dzufferey.github.io/concurrency_theory_2017/">Concurrency Theory</a>, university of Kaiserslautern, winter semester 17.</li>
<li><a href="https://dzufferey.github.io/concurrency_theory_2018/">Concurrency Theory</a>, university of Kaiserslautern, winter semester 18.</li>
<li><a href="https://dzufferey.github.io/concurrency_theory_2019/">Concurrency Theory</a>, university of Kaiserslautern, winter semester 19.</li>
<li><a href="http://es.cs.uni-kl.de/teaching/projAppVerif/index.html">Applied Verification Lab (project)</a>, university of Kaiserslautern, winter semester 18, 19, and 20.</li>
<li><a href="https://www.kis.uni-kl.de/campus/all/event.asp?gguid=0x35DAFC84AF694F4AAC03362EB305F687&tguid=0x20A24741AF3347FEB6943B4BA195534F">Advanced Automata Theory</a>, university of Kaiserslautern, summer semester 19.</li>
</ul>
</div>
</div>
</div>
<div class="container separation"></div>
<div class="container" id="sec-misc">
<h3>Awards</h3>
<ul>
<li> Excellency Scholarships at the Master level from EPFL.</li>
<li> Graduated best in class from my Bachelor at EPFL.</li>
<li> Silver Medal of the Association for Computing Machinery - International Collegiate Programming Contest (Regionals, South-Western Europe) in 2007 with EPFL (6th place, Swiss champions, team with Frédéric Dubut and Christian Kauth)</li>
<li> Bronze Medal of the Association for Computing Machinery - International Collegiate Programming Contest (Regionals, South-Western Europe) in 2006 with EPFL (9th place, Swiss champions, team with Frédéric Dubut and Abhishek Garg)</li>
</ul>
<h3>Other</h3>
<ul>
<li><a href="files/public.asc">my GPG key</a> (fingerprint: 77D7 B905 B1E6 0E27 DEB7 88B4 E355 F1D7 EDAA AE18)</li>
<li><a href="http://orcid.org/0000-0002-3197-8736">ORCID</a></li>
<li><a href="https://github.com/dzufferey">Github profile</a></li>
<li><a href="http://www.flickr.com/photos/rilaak/">Photography</a></li>
</ul>
</div>
<!-- Load the scripts at the end to be faster -->
<script src="lib/jquery/jquery-3.7.1.min.js" type="text/javascript" ></script>
<script src="lib/bootstrap/js/bootstrap.min.js" type="text/javascript" ></script>
<script src="lib/scripts.js" type="text/javascript" ></script>`
</body>
</html>