-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathindex.html
More file actions
329 lines (290 loc) · 14.2 KB
/
index.html
File metadata and controls
329 lines (290 loc) · 14.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
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<title>Daniel Larraz's Homepage</title>
<link rel="stylesheet" href="style.css" type="text/css">
</head>
<body>
<header>
<h1>Daniel Larraz</h1>
<nav role="navigation">
<p>
<a href="#about">About me</a> -
<a href="#publications">Publications</a> -
<a href="#teaching">Teaching</a> -
<a href="#contact">Contact</a>
</p>
</nav>
</header>
<div id="about">
<div id="photo"><img src="photo.jpg" alt="Photo of Daniel Larraz" width="190" height="190"></div>
<div id="introduction">
<p>I am a research scientist at the <a href="http://www.uiowa.edu">University of Iowa</a>.
My research focuses on the application of
<abbr title="Satisfiability Modulo Theories">SMT</abbr>-based techniques to the
formal verification of computer systems. I am currently working with
<a href="http://homepage.cs.uiowa.edu/~tinelli/">Cesare Tinelli</a> on the
development of automated techniques
to verify synchronous data-flow programs, and their implementation in the
model checker <a href="http://kind2-mc.github.io/kind2/">Kind 2</a>.</p>
<p>I obtained my PhD at the <a href="http://www.upc.edu">Technical University of Catalonia</a>
(<abbr title="Universitat Politècnica de Catalunya" lang="ca">UPC</abbr>) under the supervision of
<a href="https://costa.fdi.ucm.es/~arubio/">Albert Rubio</a>. For my PhD I worked on
array invariant generation, termination analysis, and compositional safety verification
of imperative programs using Max-<abbr title="Satisfiability Modulo Theories">SMT</abbr> solvers.
I also contributed to
the implementation of the <a href="http://www.cs.upc.edu/~albert/VeryMax.html">VeryMax</a> tool,
a verification framework for checking automatically safety properties, and proving (conditional)
termination and non-termination of C/C++ programs.
<p>From April through June 2014, I spent three months as a research intern at
<a href="http://research.microsoft.com/en-us/labs/cambridge/">Microsoft Research Cambridge</a>
in the <a href="http://research.microsoft.com/en-us/groups/ppt/">Programming Principles and Tools</a> group
under the supervision of
<a href="https://www.microsoft.com/en-us/research/people/rybal/">Andrey Rybalchenko</a>.</p>
</div>
</div>
<h2 id="publications">Publications</h2>
<ul class="publications">
<li>
<span class="paper-title">A Comprehensive, Automated Security Analysis of the Uptane Automotive Over-the-Air Update Framework</span>
[<a href="papers/raid24.pdf">PDF</a>].
<a href="https://lorchrob.github.io/">Robert Lorch</a>,
Daniel Larraz,
<a href="http://homepage.cs.uiowa.edu/~tinelli/">Cesare Tinelli</a>,
<a href="https://www3.cs.stonybrook.edu/~omar/">Omar Chowdhury</a>.
In <span class="conference-name">27th International Symposium on Research in Attacks, Intrusions and Defenses (<abbr title="Research in Attacks, Intrusions and Defenses">RAID</abbr>'24)</span>,
September 2024, Padua (Italy).
</li>
<li>
<span class="paper-title">CRV: Automated Cyber-Resiliency Reasoning for System Design Models</span>
[<a href="papers/fmcad23.pdf">PDF</a>].
Daniel Larraz,
<a href="https://lorchrob.github.io/">Robert Lorch</a>,
<a href="https://myweb.uiowa.edu/yahyazadeh/">Moosa Yahyazadeh</a>,
M. Fareed Arif,
<a href="https://www3.cs.stonybrook.edu/~omar/">Omar Chowdhury</a>,
<a href="http://homepage.cs.uiowa.edu/~tinelli/">Cesare Tinelli</a>.
In <span class="conference-name">23rd International Conference on Formal Methods in
Computer-Aided Design (<abbr title="Formal Methods in Computer-Aided Design">FMCAD</abbr>'23)</span>,
October 2023, Ames (USA).
</li>
<li>
<span class="paper-title">Finding Locally Smallest Cut Sets using Max-SMT</span>
[<a href="papers/hilt22-mcs.pdf">PDF</a>].
Daniel Larraz,
<a href="http://homepage.cs.uiowa.edu/~tinelli/">Cesare Tinelli</a>.
In <span class="conference-name"><abbr title="Association for Computing Machinery">ACM</abbr>
<abbr title="Special Interest Group on Ada Programming Language">SIGAda</abbr> Ada Letters</span>,
December 2022.
</li>
<li>
<span class="paper-title">Beyond model checking of idealized Lustre in Kind 2</span>
[<a href="papers/hilt22-kind2.pdf">PDF</a>].
Daniel Larraz,
<a href="https://homepage.divms.uiowa.edu/~viswanathn/">Arjun Viswanathan</a>,
Mickaël Laurent,
<a href="http://homepage.cs.uiowa.edu/~tinelli/">Cesare Tinelli</a>.
In <span class="conference-name"><abbr title="Association for Computing Machinery">ACM</abbr>
<abbr title="Special Interest Group on Ada Programming Language">SIGAda</abbr> Ada Letters</span>,
December 2022.
</li>
<li>
<span class="paper-title">VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System</span>
[<a href="papers/systems21.pdf">PDF</a>].
<a href="https://www.ge.com/research/people/baoluo-meng">Baoluo Meng</a>,
Daniel Larraz,
<a href="https://www.ge.com/research/people/kit-siu">Kit Siu</a>,
Abha Moitra,
<a href="https://www.ge.com/research/people/john-interrante">John Interrante</a>,
William Smith,
Saswata Paul,
Daniel Prince,
Heber Herencia-Zapana,
M. Fareed Arif,
<a href="https://myweb.uiowa.edu/yahyazadeh/">Moosa Yahyazadeh</a>,
Vidhya Tekken Valapil,
<a href="https://www.ge.com/research/people/michael-durling">Michael Durling</a>,
<a href="http://homepage.cs.uiowa.edu/~tinelli/">Cesare Tinelli</a>,
<a href="https://www3.cs.stonybrook.edu/~omar/">Omar Chowdhury</a>.
In <span class="conference-name">Systems</span>, March 2021.
</li>
<li>
<span class="paper-title">Merit and Blame Assignment with Kind 2</span>
[<a href="papers/fmics21.pdf">PDF</a>].
Daniel Larraz, Mickaël Laurent,
<a href="http://homepage.cs.uiowa.edu/~tinelli/">Cesare Tinelli</a>.
In <span class="conference-name">26th International Conference on Formal Methods for
Industrial Critical Systems (<abbr title="Formal Methods for Industrial Critical Systems">FMICS</abbr>'21)</span>,
August 2021, Online.
</span>
</li>
<li>
<span class="paper-title">SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces</span>
[<a href="papers/fmcad20.pdf">PDF</a>].
M. Fareed Arif, Daniel Larraz, Mitziu Echeverria,
<a href="http://homepage.cs.uiowa.edu/~ajreynol/">Andrew Reynolds</a>,
<a href="https://www3.cs.stonybrook.edu/~omar/">Omar Chowdhury</a>,
<a href="http://homepage.cs.uiowa.edu/~tinelli/">Cesare Tinelli</a>.
In <span class="conference-name">20th International Conference on Formal Methods in
Computer-Aided Design (<abbr title="Formal Methods in Computer-Aided Design">FMCAD</abbr>'20)</span>,
September 2020, Online.
</li>
<li>
<span class="paper-title">Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis</span>
[<a href="papers/ijcar20.pdf">PDF</a>].
<a href="http://homepage.cs.uiowa.edu/~ajreynol/">Andrew Reynolds</a>,
<a href="https://hanielbarbosa.com/">Haniel Barbosa</a>,
Daniel Larraz,
<a href="http://homepage.cs.uiowa.edu/~tinelli/">Cesare Tinelli</a>.
In <span class="conference-name">10th International Joint Conference on Automated Reasoning
(<abbr title="International Joint Conference on Automated Reasoning">IJCAR</abbr>'20)</span>,
July 2020, Paris (France).
</li>
<li>
<span class="paper-title">Architectural and Behavioral Analysis for Cyber Security</span>
[<a href="papers/dasc19.pdf">PDF</a>].
Kit Siu, Abha Moitra, Meng Li, Michael Durling, Heber Herencia-Zapana,
John Interrante, Baoluo Meng,
Daniel Larraz,
<a href="http://homepage.cs.uiowa.edu/~tinelli/">Cesare Tinelli</a>,
<a href="https://www3.cs.stonybrook.edu/~omar/">Omar Chowdhury</a>,
<a href="https://myweb.uiowa.edu/yahyazadeh/">Moosa Yahyazadeh</a>,
M. Fareed Arif, Daniel Prince.
In <span class="conference-name">IEEE/AIAA 38th Digital Avionics Systems Conference
(<abbr title="Digital Avionics Systems Conference">DASC</abbr>'19)</span>,
September, 2019, San Diego (USA).
</li>
<li>
<span class="paper-title">Incomplete SMT Techniques for Solving Non-Linear
Formulas over the Integers</span>
[<a href="papers/tocl.pdf">PDF</a>].
Cristina Borralleras,
Daniel Larraz,
<a href="http://www.cs.upc.edu/~oliveras/">Albert Oliveras</a>,
<a href="http://www.cs.upc.edu/~erodri/">Enric Rodríguez-Carbonell</a>,
and <a href="https://costa.fdi.ucm.es/~arubio/">Albert Rubio</a>.
In <span class="conference-name"><abbr title="Association for Computing Machinery">ACM</abbr>
Transactions on Computational Logic
(<abbr title="Transactions on Computational Logic">TOCL</abbr>)</span>,
September 2019.
</li>
<li>
<span class="paper-title">Extending enumerative function synthesis via SMT-driven classification</span>
[<a href="papers/fmcad19.pdf">PDF</a>].
<a href="https://hanielbarbosa.com/">Haniel Barbosa</a>,
<a href="http://homepage.cs.uiowa.edu/~ajreynol/">Andrew Reynolds</a>,
Daniel Larraz,
<a href="http://homepage.cs.uiowa.edu/~tinelli/">Cesare Tinelli</a>.
In <span class="conference-name">19th International Conference on Formal Methods in
Computer-Aided Design (<abbr title="Formal Methods in Computer-Aided Design">FMCAD</abbr>'19)</span>,
October 2019, San Jose (USA).
</li>
<li>
<span class="paper-title">Proving Termination through Conditional Termination</span>
[<a href="papers/tacas17.pdf">PDF</a>].
Cristina Borralleras,
<a href="http://research.microsoft.com/en-us/people/mabrocks/">Marc Brockschmidt</a>,
Daniel Larraz,
<a href="http://www.cs.upc.edu/~oliveras/">Albert Oliveras</a>,
<a href="http://www.cs.upc.edu/~erodri/">Enric Rodríguez-Carbonell</a>,
and <a href="https://costa.fdi.ucm.es/~arubio/">Albert Rubio</a>.
In <span class="conference-name">23rd International Conference on Tools and Algorithms for
the Construction and Analysis of Systems
(<abbr title="Tools and Algorithms for the Construction and Analysis of Systems">TACAS</abbr>'17)</span>,
April 2017, Uppsala (Sweden). <a href="http://www.springer.de/comp/lncs/index.html">© Springer-Verlag</a>.
</li>
<li>
<span class="paper-title">Speeding Up the Constraint-Based Method in Difference Logic</span>
[<a href="papers/sat16.pdf">PDF</a>].
Lorenzo Candeago, Daniel Larraz,
<a href="http://www.cs.upc.edu/~oliveras/">Albert Oliveras</a>,
<a href="http://www.cs.upc.edu/~erodri/">Enric Rodríguez-Carbonell</a>
and <a href="https://costa.fdi.ucm.es/~arubio/">Albert Rubio</a>.
In <span class="conference-name">19th International Conference on Theory and
Applications of Satisfiability Testing (SAT'16)</span>,
July 2016, Bordeaux (France). <a href="http://www.springer.de/comp/lncs/index.html">© Springer-Verlag</a>.
</li>
<li>
<span class="paper-title">Compositional Safety Verification with Max-SMT</span>
[<a href="papers/fmcad15.pdf">PDF</a>].
<a href="http://research.microsoft.com/en-us/people/mabrocks/">Marc Brockschmidt</a>,
Daniel Larraz,
<a href="http://www.cs.upc.edu/~oliveras/">Albert Oliveras</a>,
<a href="http://www.cs.upc.edu/~erodri/">Enric Rodríguez-Carbonell</a>
and <a href="https://costa.fdi.ucm.es/~arubio/">Albert Rubio</a>.
In <span class="conference-name">15th Formal Methods in Computer-Aided Design
(<abbr title="Formal Methods in Computer-Aided Design">FMCAD</abbr>'15)</span>,
September 2015, Austin (USA). © ACM/IEEE.
</li>
<li>
<span class="paper-title">Proving Non-termination Using Max-SMT</span>
[<a href="papers/cav14.pdf">PDF</a>].
Daniel Larraz,
<a href="http://www0.cs.ucl.ac.uk/staff/K.Nimkar/">Kaustubh Nimkar</a>,
<a href="http://www.cs.upc.edu/~oliveras/">Albert Oliveras</a>,
<a href="http://www.cs.upc.edu/~erodri/">Enric Rodríguez-Carbonell</a>
and <a href="https://costa.fdi.ucm.es/~arubio/">Albert Rubio</a>.
In <span class="conference-name">26th International Conference on Computer
Aided Verification (<abbr title="Computer
Aided Verification">CAV</abbr>'14)</span>, July 2014, Vienna (Austria).
<a href="http://www.springer.de/comp/lncs/index.html">© Springer-Verlag</a>.
</li>
<li>
<span class="paper-title">Minimal-Model-Guided Approaches to Solving Polynomial
Constraints and Extensions</span>
[<a href="papers/sat14.pdf">PDF</a>].
Daniel Larraz,
<a href="http://www.cs.upc.edu/~oliveras/">Albert Oliveras</a>,
<a href="http://www.cs.upc.edu/~erodri/">Enric Rodríguez-Carbonell</a>
and <a href="https://costa.fdi.ucm.es/~arubio/">Albert Rubio</a>.
In <span class="conference-name">17th International Conference on Theory and
Applications of Satisfiability Testing (SAT'14)</span>,
July 2014, Vienna (Austria). <a href="http://www.springer.de/comp/lncs/index.html">© Springer-Verlag</a>.
</li>
<li>
<span class="paper-title">
Proving Termination of Imperative Programs Using Max-SMT</span>
[<a href="papers/fmcad13.pdf">PDF</a>].
Daniel Larraz,
<a href="http://www.cs.upc.edu/~oliveras/">Albert Oliveras</a>,
<a href="http://www.cs.upc.edu/~erodri/">Enric Rodríguez-Carbonell</a> and
<a href="https://costa.fdi.ucm.es/~arubio/">Albert Rubio</a>.
In <span class="conference-name">13th Formal Methods in Computer-Aided Design
(<abbr title="Formal Methods in Computer-Aided Design">FMCAD</abbr>'13)</span>,
October 2013, Portland, <abbr title="Oregon">OR</abbr> (USA). © ACM/IEEE.
</li>
<li>
<span class="paper-title">SMT-Based Array Invariant Generation</span>
[<a href="papers/vmcai13.pdf">PDF</a>].
Daniel Larraz,
<a href="http://www.cs.upc.edu/~erodri/">Enric Rodríguez-Carbonell</a> and
<a href="https://costa.fdi.ucm.es/~arubio/">Albert Rubio</a>.
In <span class="conference-name">14th International Conference on Verification,
Model Checking, and Abstract Interpretation
(<abbr title="Verification, Model Checking, and Abstract Interpretation">VMCAI</abbr>'13)</span>,
January 2013, Rome (Italy). <a href="http://www.springer.de/comp/lncs/index.html">© Springer-Verlag</a>.
</li>
</ul>
<h2 id="teaching">Teaching Assistant</h2>
<a href="http://www.fib.upc.edu/en/estudiar-enginyeria-informatica/assignatures/LP.html">
Programming Languages</a> at
<a href="http://www.upc.edu"><abbr title="Universitat Politècnica de Catalunya" lang="ca">UPC</abbr></a>,
(2014-2015, Bachelor in Informatics Engineering).
<h2 id="contact">Contact</h2>
<p>Email: daniel-larraz at
<span class="hidden-note">(replace at with @)</span>
<span>uiowa</span>.edu<br>
Phone: +1-319-467-0655<br>
Office: 1 <a href="https://www.facilities.uiowa.edu/named-building/jessup-hall">Jessup Hall</a>, Room F</p>
<p>Mailing address:<br>
<a href="http://www.cs.uiowa.edu">Department of Computer Science</a><br>
<a href="http://www.uiowa.edu">The University of Iowa</a><br>
14 <a href="http://maps.uiowa.edu/mlh">MacLean Hall</a><br>
Iowa City, IA 52242<br>
USA</p>
<hr>
<p>Last updated: October 23, 2024</p>
</body>
</html>