-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy patheditions.html
More file actions
549 lines (541 loc) · 70.3 KB
/
Copy patheditions.html
File metadata and controls
549 lines (541 loc) · 70.3 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
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<title>Editions — ARCH-COMP</title>
<meta name="description" content="Every ARCH edition, year by year: program, benchmarks, tool presentations, experience reports, proceedings, and repeatability packages — 2014 through 2027.">
<link rel="canonical" href="https://arch-comp.github.io/editions.html">
<meta name="theme-color" content="#2563eb">
<link rel="icon" href="images/favicon.ico" sizes="any">
<link rel="icon" href="images/favicon.svg" type="image/svg+xml">
<link rel="apple-touch-icon" href="images/apple-touch-icon.png">
<link rel="stylesheet" href="styles.css">
<link rel="preconnect" href="https://fonts.googleapis.com">
<link rel="preconnect" href="https://fonts.gstatic.com" crossorigin>
<link href="https://fonts.googleapis.com/css2?family=Inter:wght@300;400;500;600;700&display=swap" rel="stylesheet">
</head>
<body>
<a href="#main" class="skip-link">Skip to main content</a>
<header class="header">
<div class="container">
<div class="header-content">
<a href="index.html" class="logo" aria-label="ARCH-COMP home">
<img src="images/logo-white.svg" alt="ARCH" class="logo-img" width="300" height="100">
<span class="logo-word">ARCH-COMP</span>
</a>
<p class="tagline">Applied Verification of Continuous and Hybrid Systems</p>
</div>
<nav class="nav" aria-label="Primary">
<ul class="nav-list">
<li><a href="index.html#about">About</a></li>
<li><a href="index.html#categories">Categories</a></li>
<li><a href="index.html#organizers">Organizers</a></li>
<li><a href="index.html#contact">Contact</a></li>
<li class="nav-sep" aria-hidden="true"></li>
<li><a href="participate.html" class="to-page">Participate</a></li>
<li><a href="editions.html" class="to-page">Editions</a></li>
</ul>
</nav>
</div>
</header>
<main class="main subpage" id="main">
<div class="container">
<div class="breadcrumb"><a href="index.html">Home</a> / Editions</div>
<h1 class="subpage-title">Editions</h1>
<p class="subpage-lead">
Every ARCH edition, year by year — program, benchmarks, tool presentations,
experience reports, and proceedings. Pick a year to see everything from that edition.
Material before 2017 predates the friendly competition; it comes from the ARCH workshop
(migrated from <a href="https://cps-vo.org/group/ARCH" class="researcher-link" target="_blank" rel="noopener">CPS-VO</a>).
</p>
<div class="year-picker">
<label for="year-select">Edition:</label>
<select id="year-select" class="year-select" aria-label="Choose an ARCH edition year">
<option value="2027" selected>ARCH 2027 — Upcoming</option>
<option value="2026">ARCH 2026</option>
<option value="2025">ARCH 2025</option>
<option value="2024">ARCH 2024</option>
<option value="2023">ARCH 2023</option>
<option value="2022">ARCH 2022</option>
<option value="2021">ARCH 2021</option>
<option value="2020">ARCH 2020</option>
<option value="2019">ARCH 2019</option>
<option value="2018">ARCH 2018</option>
<option value="2017">ARCH 2017</option>
<option value="2016">ARCH 2016</option>
<option value="2015">ARCH 2015</option>
<option value="2014">ARCH 2014</option>
</select>
</div>
<section class="edition" id="y2027" data-year="2027">
<div class="edition-head"><h2 class="subpage-title">ARCH 2027 <span class="edition-badge">Upcoming</span></h2><p class="edition-when">June 2, 2027 · Online</p></div>
<h3 class="file-year">Program</h3>
<p class="section-text">The detailed program — session titles, speakers, and times — will be announced in <strong>mid-May 2027</strong>. The workshop is a public event; no registration is required.</p><div class="facts"><div><strong>Join:</strong> <a href="https://bbb.cit.tum.de/mat-jva-v7f" class="researcher-link" target="_blank" rel="noopener">bbb.cit.tum.de/mat-jva-v7f</a></div></div>
<h3 class="file-year">Call for Submissions</h3>
<p class="section-text">The workshop invites benchmark proposals, tool presentations, experience
reports, and competition results. Papers are ideally 3–8 pages, submitted via
<a href="https://easychair.org/conferences/?conf=arch27" target="_blank" rel="noopener">EasyChair (arch27)</a>
and published in the EPiC Series in Computing (DBLP-indexed).</p>
<div class="facts">
<div><strong>Submission:</strong> April 1, 2027</div>
<div><strong>Notification:</strong> April 28, 2027</div>
<div><strong>Final version:</strong> May 26, 2027</div>
</div>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="participate.html">How to participate</a></div></div>
</section>
<section class="edition" id="y2026" data-year="2026" hidden>
<div class="edition-head"><h2 class="subpage-title">ARCH 2026</h2><p class="edition-when">June 3, 2026 · ARCH workshop</p></div>
<h3 class="file-year">Program</h3>
<div class="table-wrap"><table class="program-table"><tbody>
<tr><td class="program-time">15:00 - 15:30</td><td class="program-topic">Contributed Paper (12 min presentation, 8 min discussion)</td></tr>
<tr><td class="program-time">15:00</td><td class="program-topic">Welcome Address</td></tr>
<tr><td class="program-time">15:10</td><td class="program-topic">Ludovico Battista, Stefano Tonetta and Gianni Zampedri: SpaceEx Hybrid Models with LTL Properties (Benchmark Proposal)</td></tr>
<tr><td class="program-time">15:30 - 16:30</td><td class="program-topic">Results of the ARCH Friendly Competition (7 min presentation, 3 min discussion)</td></tr>
<tr><td class="program-time">15:30</td><td class="program-topic">Piecewise Constant Dynamics (lead: Lei Bu)</td></tr>
<tr><td class="program-time">15:40</td><td class="program-topic">Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)</td></tr>
<tr><td class="program-time">15:50</td><td class="program-topic">Nonlinear Systems (lead: Luca Geretti)</td></tr>
<tr><td class="program-time">16:00</td><td class="program-topic">Falsification (lead: Claudio Menghi)</td></tr>
<tr><td class="program-time">16:10</td><td class="program-topic">Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)</td></tr>
<tr><td class="program-time">16:20</td><td class="program-topic">Hybrid Programs (lead: Stefan Mitsch)</td></tr>
</tbody></table></div>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="https://easychair.org/publications/volume/ARCH26" target="_blank" rel="noopener">EPiC proceedings volume</a></div></div>
</section>
<section class="edition" id="y2025" data-year="2025" hidden>
<div class="edition-head"><h2 class="subpage-title">ARCH 2025</h2><p class="edition-when">June 4, 2025 · Online</p></div>
<h3 class="file-year">Program</h3>
<div class="table-wrap"><table class="program-table"><tbody>
<tr><td class="program-time">16:00</td><td class="program-topic">Welcome Address</td></tr>
<tr><td class="program-time">16:10</td><td class="program-topic">Piecewise Constant Dynamics (lead: Lei Bu)</td></tr>
<tr><td class="program-time">16:20</td><td class="program-topic">Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)</td></tr>
<tr><td class="program-time">16:30</td><td class="program-topic">Nonlinear Systems (lead: Luca Geretti)</td></tr>
<tr><td class="program-time">16:40</td><td class="program-topic">Falsification (lead: Claudio Menghi)</td></tr>
<tr><td class="program-time">16:50</td><td class="program-topic">Stochastic Models (lead: Abolfazl Lavaei)</td></tr>
<tr><td class="program-time">17:00</td><td class="program-topic">Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)</td></tr>
<tr><td class="program-time">17:10</td><td class="program-topic">Hybrid Programs (lead: Stefan Mitsch)</td></tr>
<tr><td class="program-time">17:20</td><td class="program-topic">Repeatability Evaluation (lead: Tobias Ladner)</td></tr>
<tr><td class="program-time">17:30</td><td class="program-topic">Voting for ARCH 2025 Best Result Award</td></tr>
</tbody></table></div>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="https://easychair.org/publications/volume/ARCH25" target="_blank" rel="noopener">EPiC proceedings volume</a></div><div><a href="https://gitlab.com/goranf/ARCH-COMP/-/tree/master/2025" target="_blank" rel="noopener">Repeatability packages</a></div></div>
</section>
<section class="edition" id="y2024" data-year="2024" hidden>
<div class="edition-head"><h2 class="subpage-title">ARCH 2024</h2><p class="edition-when">July 3, 2024 · Boulder, USA</p></div>
<h3 class="file-year">Program</h3>
<div class="table-wrap"><table class="program-table"><tbody>
<tr><td class="program-time">12:30 - 14:00</td><td class="program-topic">Lunch</td></tr>
<tr><td class="program-time">14:00 - 15:20</td><td class="program-topic">Contributed Papers (12 min presentation, 8 min discussion)</td></tr>
<tr><td class="program-time">14:00</td><td class="program-topic">Welcome Address</td></tr>
<tr><td class="program-time">14:20</td><td class="program-topic">Stylianos Basagiannis, Ludovico Battista, Anna Becchi, Alessandro Cimatti, Georgios Giantamidis, Sergio Mover, Alberto Tacchella, Stefano Tonetta and Vassilios Tsachouridis: Stability Verification of an Industrial Switched PI Control Systems (Benchmark Proposal)</td></tr>
<tr><td class="program-time">14:40</td><td class="program-topic">Mark Wetzlinger and Matthias Althoff: Randomized Generation of Arbitrarily Difficult Verification Tasks for Linear Time-Invariant Systems (Benchmark Proposal)</td></tr>
<tr><td class="program-time">15.00</td><td class="program-topic">Mark Wetzlinger, Viktor Kotsev, Adrian Kulmburg and Matthias Althoff: Implementation of Polyhedral Operations in CORA 2024 (Tool Presentation)</td></tr>
<tr><td class="program-time">15:20 - 15:40</td><td class="program-topic">Results of the ARCH Friendly Competition (Part I)</td></tr>
<tr><td class="program-time">15:20</td><td class="program-topic">Nonlinear Systems (lead: Luca Geretti)</td></tr>
<tr><td class="program-time">15:30</td><td class="program-topic">Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)</td></tr>
<tr><td class="program-time">15:40 - 16:10</td><td class="program-topic">Coffee Break</td></tr>
<tr><td class="program-time">16:10 - 17:00</td><td class="program-topic">Results of the ARCH Friendly Competition (Part II)</td></tr>
<tr><td class="program-time">16:10</td><td class="program-topic">Piecewise Constant Dynamics (lead: Lei Bu)</td></tr>
<tr><td class="program-time">16:20</td><td class="program-topic">Falsification (lead: Claudio Menghi)</td></tr>
<tr><td class="program-time">16:30</td><td class="program-topic">Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)</td></tr>
<tr><td class="program-time">16:40</td><td class="program-topic">Voting for ARCH 2024 Best Result Award</td></tr>
</tbody></table></div>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="https://easychair.org/publications/volume/ARCH-COMP24" target="_blank" rel="noopener">EPiC proceedings volume</a></div><div><a href="https://gitlab.com/goranf/ARCH-COMP/-/tree/master/2024" target="_blank" rel="noopener">Repeatability packages</a></div></div>
</section>
<section class="edition" id="y2023" data-year="2023" hidden>
<div class="edition-head"><h2 class="subpage-title">ARCH 2023</h2><p class="edition-when">May 9, 2023 · San Antonio, USA</p></div>
<h3 class="file-year">Program</h3>
<div class="table-wrap"><table class="program-table"><tbody>
<tr><td class="program-time">08:00 - 09:00</td><td class="program-topic">Breakfast/Continental Zoom Link: <a href="https://zoom.us/j/97903297749" target="_blank" rel="noopener">https://zoom.us/j/97903297749</a></td></tr>
<tr><td class="program-time">09:00 - 10:00</td><td class="program-topic">Contributed Papers (12 min presentation, 8 min discussion)</td></tr>
<tr><td class="program-time">09:00</td><td class="program-topic">Goran Frehse: Welcome Address</td></tr>
<tr><td class="program-time">09:20</td><td class="program-topic">Sanaz Sheikhi and Stanley Bak: Closed-Loop ACAS Xu Neural Network Verification (Benchmark Proposal)</td></tr>
<tr><td class="program-time">09:40</td><td class="program-topic">Matthias Althoff: Checking and Establishing Reachset Conformance in CORA 2023</td></tr>
<tr><td class="program-time">10:00 - 10:30</td><td class="program-topic">Coffee Break</td></tr>
<tr><td class="program-time">10:30 - 12:00</td><td class="program-topic">Results of the ARCH Friendly Competition</td></tr>
<tr><td class="program-time">10:30</td><td class="program-topic">Piecewise Constant Dynamics (lead: Lei Bu)</td></tr>
<tr><td class="program-time">10:40</td><td class="program-topic">Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)</td></tr>
<tr><td class="program-time">10:50</td><td class="program-topic">Nonlinear Systems (lead: Luca Geretti)</td></tr>
<tr><td class="program-time">11:00</td><td class="program-topic">Stochastic Models (lead: Alessandro Abate)</td></tr>
<tr><td class="program-time">11:10</td><td class="program-topic">Falsification (lead: Gidon Ernst)</td></tr>
<tr><td class="program-time">11:20</td><td class="program-topic">Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)</td></tr>
<tr><td class="program-time">11:30</td><td class="program-topic">Hybrid Programs (lead: Stefan Mitsch)</td></tr>
<tr><td class="program-time">11:40</td><td class="program-topic">Voting for ARCH 2023 Best Result Award</td></tr>
</tbody></table></div>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="https://easychair.org/publications/volume/ARCH23" target="_blank" rel="noopener">EPiC proceedings volume</a></div><div><a href="https://gitlab.com/goranf/ARCH-COMP/-/tree/master/2023" target="_blank" rel="noopener">Repeatability packages</a></div></div>
</section>
<section class="edition" id="y2022" data-year="2022" hidden>
<div class="edition-head"><h2 class="subpage-title">ARCH 2022</h2><p class="edition-when">September 6, 2022 · Munich, Germany</p></div>
<h3 class="file-year">Program</h3>
<p class="section-text">Since we will have a hybrid event (remote and in-person participation), we shortened the program to accommodate as many time zones as possible. All workshops at SAFECOMP have to end before 17.00 so that participants can join the evening event in downtown Munich at 18.30. 12:30-13:30 (CEST) Lunch Break (Lunch is offered for all participants who have registered as on-site present) 14:00-15:00 (CEST) Contributed Papers (10 min presentation, 5 min discussion)</p>
<div class="table-wrap"><table class="program-table"><tbody>
<tr><td class="program-time">14:00</td><td class="program-topic">Goran Frehse: Welcome Address</td></tr>
<tr><td class="program-time">14:15</td><td class="program-topic">Mostafa Ayesh, Namya Mehan, Ethan Dhanraj, Abdul El-Rahwan, Simon Emil Opalka, Tony Fan, Akil Hamilton, Akshay Mathews Jacob, Rahul Anthony Sundarrajan, Bryan Widjaja and Claudio Menghi: Two Simulink Models with Requirements for a Simple Controller of a Pacemaker Device</td></tr>
<tr><td class="program-time">14:30</td><td class="program-topic">Matthias Althoff: Benchmarks for the Formal Verification of Power Systems</td></tr>
<tr><td class="program-time">14:45</td><td class="program-topic">Victor Gassmann and Matthias Althoff: Implementation of Ellipsoidal Operations in CORA 2022</td></tr>
<tr><td class="program-time">15:00-15:30 (CEST)</td><td class="program-topic">Coffee Break</td></tr>
<tr><td class="program-time">15:30-17:00 (CEST)</td><td class="program-topic">Results of the ARCH Friendly Competition</td></tr>
<tr><td class="program-time">15:30</td><td class="program-topic">Piecewise Constant Dynamics (lead: Lei Bu)</td></tr>
<tr><td class="program-time">15:40</td><td class="program-topic">Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)</td></tr>
<tr><td class="program-time">15:50</td><td class="program-topic">Nonlinear Systems (lead: Luca Geretti)</td></tr>
<tr><td class="program-time">16:00</td><td class="program-topic">Stochastic Models (lead: Alessandro Abate)</td></tr>
<tr><td class="program-time">16:10</td><td class="program-topic">Falsification (lead: Gidon Ernst)</td></tr>
<tr><td class="program-time">16:20</td><td class="program-topic">Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)</td></tr>
<tr><td class="program-time">16:30</td><td class="program-topic">Hybrid Programs (lead: Stefan Mitsch)</td></tr>
<tr><td class="program-time">16.40</td><td class="program-topic">Voting for ARCH 2022 Best Result Award</td></tr>
<tr><td class="program-time">16.50</td><td class="program-topic">Discussion on the future of the friendly competition</td></tr>
</tbody></table></div>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="https://easychair.org/publications/volume/ARCH22" target="_blank" rel="noopener">EPiC proceedings volume</a></div><div><a href="https://gitlab.com/goranf/ARCH-COMP/-/tree/master/2022" target="_blank" rel="noopener">Repeatability packages</a></div></div>
</section>
<section class="edition" id="y2021" data-year="2021" hidden>
<div class="edition-head"><h2 class="subpage-title">ARCH 2021</h2><p class="edition-when">July 9, 2021 · Online</p></div>
<h3 class="file-year">Program</h3>
<p class="section-text">Since we will have a live online event, we shortened the program to accommodate as many time zones as possible. <a href="https://bbb.in.tum.de/mat-9xz-qq5-m8n" target="_blank" rel="noopener">Recording of the workshop</a>. 16:30-17:30 (CEST) Contributed Papers (10 min presentation, 5 min discussion)</p>
<div class="table-wrap"><table class="program-table"><tbody>
<tr><td class="program-time">16:30</td><td class="program-topic">Zahra Ramezani, Alexandre Donze, Martin Fabian and Knut Akesson: Temporal Logic Falsification of Cyber-Physical Systems using Input Pulse Generators</td></tr>
<tr><td class="program-time">16:45</td><td class="program-topic">Niklas Kochdumper, Philipp Gassert and Matthias Althoff: Verification of Collision Avoidance for CommonRoad Traffic Scenarios</td></tr>
<tr><td class="program-time">17:00</td><td class="program-topic">Jawher Jerray: ORBITADOR: A tool to analyze the stability of periodical dynamical systems</td></tr>
<tr><td class="program-time">17:15</td><td class="program-topic">Matthias Althoff: Guaranteed State Estimation in CORA 2021</td></tr>
<tr><td class="program-time">17:30-18:30 (CEST)</td><td class="program-topic">Plenary Talk of Paulo Tabuada</td></tr>
<tr><td class="program-time">18:30-19:30 (CEST)</td><td class="program-topic">Results of the ARCH Friendly Competition</td></tr>
<tr><td class="program-time">18:30</td><td class="program-topic">Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)</td></tr>
<tr><td class="program-time">18:40</td><td class="program-topic">Nonlinear Systems (lead: Luca Geretti)</td></tr>
<tr><td class="program-time">18:50</td><td class="program-topic">Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)</td></tr>
<tr><td class="program-time">19:00</td><td class="program-topic">Stochastic Models (lead: Alessandro Abate)</td></tr>
<tr><td class="program-time">19:10</td><td class="program-topic">Falsification (lead: Gidon Ernst)</td></tr>
<tr><td class="program-time">19:20</td><td class="program-topic">Hybrid Programs (lead: Stefan Mitsch)</td></tr>
<tr><td class="program-time">19:30-19:35 (CEST)</td><td class="program-topic">Break</td></tr>
<tr><td class="program-time">19:35</td><td class="program-topic">Voting for ARCH 2021 Best Result Award</td></tr>
<tr><td class="program-time">19:40</td><td class="program-topic">Discussion on the future of the friendly competition</td></tr>
</tbody></table></div>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="https://easychair.org/publications/volume/ARCH21" target="_blank" rel="noopener">EPiC proceedings volume</a></div><div><a href="https://gitlab.com/goranf/ARCH-COMP/-/tree/master/2021" target="_blank" rel="noopener">Repeatability packages</a></div></div>
</section>
<section class="edition" id="y2020" data-year="2020" hidden>
<div class="edition-head"><h2 class="subpage-title">ARCH 2020</h2><p class="edition-when">July 12, 2020 · Online</p></div>
<h3 class="file-year">Program</h3>
<p class="section-text">Since this was a live and online workshop, we shortened the program to accomodate as many time zones as possible. <a href="https://bbb.in.tum.de/mat-xyp-ddk" target="_blank" rel="noopener">Recordings of the workshop.</a> 17:00-18:30 (CEST) Contributed Papers (tentative; 10 min presentation, 5 min discussion)</p>
<div class="table-wrap"><table class="program-table"><tbody>
<tr><td class="program-time">17:00</td><td class="program-topic">Jawher Jerray, Laurent Fribourg and Étienne André: Guaranteed phase synchronization of hybrid oscillators using symbolic Euler's method</td></tr>
<tr><td class="program-time">17:15</td><td class="program-topic">Johan Lidén Eddeland, Sajed Miremadi and Knut Åkesson: Evaluating Optimization Solvers and Robust Semantics for Simulation-Based Falsification</td></tr>
<tr><td class="program-time">17:30</td><td class="program-topic">Johan Lidén Eddeland, Alexandre Donzé, Sajed Miremadi and Knut Åkesson: Industrial Temporal Logic Specifications for Falsification of Cyber-Physical Systems</td></tr>
<tr><td class="program-time">17:45</td><td class="program-topic">Maximilian Gaukler: Analysis of Real-Time Control Systems using First-Order Continuization</td></tr>
<tr><td class="program-time">18:00</td><td class="program-topic">Ian Mitchell: A Robust Controlled Backward Reach Tube with (Almost) Analytic Solution for Two Dubins Cars</td></tr>
<tr><td class="program-time">18:15</td><td class="program-topic">Edward Kim and Parasara Sridhar Duggirala: Kaa: A Python Implementation of Reachable Set Computation Using Bernstein Polynomials</td></tr>
<tr><td class="program-time">18:30-18:45 (CEST)</td><td class="program-topic">Break</td></tr>
<tr><td class="program-time">18:45</td><td class="program-topic">Taylor Johnson: Tour through our online repository</td></tr>
<tr><td class="program-time">19:00-20:10 (CEST)</td><td class="program-topic">Results of the ARCH Friendly Competition</td></tr>
<tr><td class="program-time">19:00</td><td class="program-topic">Piecewise Constant Dynamics plus BMC (lead: Lei Bu)</td></tr>
<tr><td class="program-time">19:10</td><td class="program-topic">Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)</td></tr>
<tr><td class="program-time">19:20</td><td class="program-topic">Nonlinear Systems (lead: Luca Geretti)</td></tr>
<tr><td class="program-time">19:30</td><td class="program-topic">Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)</td></tr>
<tr><td class="program-time">19:40</td><td class="program-topic">Stochastic Models (lead: Alessandro Abate)</td></tr>
<tr><td class="program-time">19:50</td><td class="program-topic">Falsification (lead: Gidon Ernst)</td></tr>
<tr><td class="program-time">20:00</td><td class="program-topic">Hybrid Programs (lead: Stefan Mitsch)</td></tr>
<tr><td class="program-time">20:10-20:15 (CEST)</td><td class="program-topic">Break</td></tr>
<tr><td class="program-time">20:15</td><td class="program-topic">Discussion on the future of the friendly competition</td></tr>
</tbody></table></div>
<h3 class="file-year">Benchmarks</h3>
<ul class="file-list">
<li class="file-item"><span class="file-title">Benchmark package 5</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH20_Attachment_5zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark package 7</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH20_Attachment_7zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
</ul>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="https://easychair.org/publications/volume/ARCH20" target="_blank" rel="noopener">EPiC proceedings volume</a></div><div><a href="https://gitlab.com/goranf/ARCH-COMP/-/tree/master/2020" target="_blank" rel="noopener">Repeatability packages</a></div></div>
</section>
<section class="edition" id="y2019" data-year="2019" hidden>
<div class="edition-head"><h2 class="subpage-title">ARCH 2019</h2><p class="edition-when">April 15, 2019 · Montreal, Canada</p></div>
<h3 class="file-year">Program</h3>
<div class="table-wrap"><table class="program-table"><tbody>
<tr><td class="program-time">07:00-08:30</td><td class="program-topic">Registration</td></tr>
<tr><td class="program-time">8:30</td><td class="program-topic">Invited Talk I: Nathalie Cauchi - Tools for Stochastic Hybrid Systems Quo Vadis</td></tr>
<tr><td class="program-time">09:30-10:00</td><td class="program-topic">Results of the ARCH Friendly Competition I</td></tr>
<tr><td class="program-time">09:30</td><td class="program-topic">Piecewise Constant Dynamics (lead: Goran Frehse)</td></tr>
<tr><td class="program-time">09:40</td><td class="program-topic">Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)</td></tr>
<tr><td class="program-time">09:50</td><td class="program-topic">Nonlinear Dynamics (lead: Fabian Immler)</td></tr>
<tr><td class="program-time">10:00-10:30</td><td class="program-topic">Coffee Break</td></tr>
<tr><td class="program-time">10:30-12:00</td><td class="program-topic">Results of the ARCH Friendly Competition II and Contributed Papers</td></tr>
<tr><td class="program-time">10:30</td><td class="program-topic">Stochastic Models (lead: Alessandro Abate)</td></tr>
<tr><td class="program-time">10:40</td><td class="program-topic">Bounded Model Checking (lead: Lei Bu)</td></tr>
<tr><td class="program-time">10:50</td><td class="program-topic">Falsification (lead: Gidon Ernst)</td></tr>
<tr><td class="program-time">11:00</td><td class="program-topic">Hybrid Programs (lead: Stefan Mitsch)</td></tr>
<tr><td class="program-time">11:10</td><td class="program-topic">AI category (lead: Taylor Johnson)</td></tr>
<tr><td class="program-time">11:20</td><td class="program-topic">Sophie Gruenbacher, Jacek Cyranka, Md Ariful Islam, Max Tschaikowski, Scott Smolka and Radu Grosu: Under the Hood of a Stand-Alone Lagrangian Reachability Tool</td></tr>
<tr><td class="program-time">11:40</td><td class="program-topic">Stanley Bak and Kerianne Hobbs: Efficient n-to-n Collision Detection for Space Debris using 4D AABB Trees</td></tr>
<tr><td class="program-time">12:00-13:30</td><td class="program-topic">Lunch</td></tr>
<tr><td class="program-time">13:30-15:00</td><td class="program-topic">Invited Talk II, Benckmark Proposals, and Discussion on Benchmark Formats</td></tr>
<tr><td class="program-time">13:30</td><td class="program-topic">Invited Talk II: Taylor Johnson - Verification for Autonomous Cyber-Physical Systems with Machine Learning Components</td></tr>
<tr><td class="program-time">14:30</td><td class="program-topic">Maximilian Gaukler and Peter Ulbrich: Worst-Case Analysis of Digital Control Loops with Uncertain Input/Output Timing (benchmark proposal)</td></tr>
<tr><td class="program-time">14:40</td><td class="program-topic">Diego Manzanas Lopez, Patrick Musau, Hoang Dung Tran and Taylor T Johnson: Verification of Closed-loop Systems with Neural Network Controllers (benchmark proposal)</td></tr>
<tr><td class="program-time">14:50</td><td class="program-topic">Discussion on Benchmark Formats</td></tr>
<tr><td class="program-time">15:30-16:00</td><td class="program-topic">Coffee Break</td></tr>
<tr><td class="program-time">16:00</td><td class="program-topic">Discussion on Repeatability Evaluation</td></tr>
</tbody></table></div>
<h3 class="file-year">Benchmarks</h3>
<ul class="file-list">
<li class="file-item"><span class="file-title">Benchmark package 2</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH19_Attachment_2zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark package 3</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH19_Attachment_3zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
</ul>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="https://easychair.org/publications/volume/ARCH19" target="_blank" rel="noopener">EPiC proceedings volume</a></div><div><a href="https://gitlab.com/goranf/ARCH-COMP/-/tree/master/2019" target="_blank" rel="noopener">Repeatability packages</a></div></div>
</section>
<section class="edition" id="y2018" data-year="2018" hidden>
<div class="edition-head"><h2 class="subpage-title">ARCH 2018</h2><p class="edition-when">July 13, 2018 · Oxford, UK</p></div>
<h3 class="file-year">Program</h3>
<p class="section-text">09:00-10:00 Invited Talk</p>
<div class="table-wrap"><table class="program-table"><tbody>
<tr><td class="program-time">9:00</td><td class="program-topic">Erika Abraham - Old-established methods in a new look: How HyPro speeds up reachability computations for hybrid systems</td></tr>
<tr><td class="program-time">10:50-12:00</td><td class="program-topic">Results of the ARCH friendly competition</td></tr>
<tr><td class="program-time">10:50</td><td class="program-topic">Piecewise Constant Dynamics (lead: Goran Frehse)</td></tr>
<tr><td class="program-time">11:00</td><td class="program-topic">Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)</td></tr>
<tr><td class="program-time">11:10</td><td class="program-topic">Nonlinear Dynamics (lead: Fabian Immler)</td></tr>
<tr><td class="program-time">11:20</td><td class="program-topic">Stochastic Models (lead: Alessandro Abate)</td></tr>
<tr><td class="program-time">11:30</td><td class="program-topic">Bounded Model Checking (lead: Lei Bu)</td></tr>
<tr><td class="program-time">11:40</td><td class="program-topic">Falsification (lead: Georgios Fainekos)</td></tr>
<tr><td class="program-time">11:50</td><td class="program-topic">Hybrid Programs (lead: Stefan Mitsch)</td></tr>
<tr><td class="program-time">12:00-14:00</td><td class="program-topic">Lunch</td></tr>
<tr><td class="program-time">14:00-15:10</td><td class="program-topic">Tools and Benchmarks I</td></tr>
<tr><td class="program-time">14:00</td><td class="program-topic">Stanley Bak: Verifying 10000-dimensional Linear Systems 10000x Faster</td></tr>
<tr><td class="program-time">14:20</td><td class="program-topic">Matthias Althoff, Dmitry Grebenyuk and Niklas Kochdumper: Implementation of Taylor models in CORA 2018</td></tr>
<tr><td class="program-time">14:40</td><td class="program-topic">Peter Heidlauf, Alexander Collins, Michael Bolender and Stanley Bak: Verification Challenges in F-16 Ground Collision Avoidance and Other Automated Maneuvers</td></tr>
<tr><td class="program-time">14:55</td><td class="program-topic">Kerianne Hobbs, Peter Heidlauf, Alexander Collins and Stanley Bak: Space Debris Collision Detection using Reachability</td></tr>
<tr><td class="program-time">15:10-15:45</td><td class="program-topic">Coffee break</td></tr>
<tr><td class="program-time">15:45-17:00</td><td class="program-topic">Benchmarks II</td></tr>
<tr><td class="program-time">15:45</td><td class="program-topic">Patrick Musau and Taylor T Johnson: Benchmark: Continuous-Time Recurrent Neural Networks</td></tr>
<tr><td class="program-time">16:00</td><td class="program-topic">Patrick Musau, Diego Manzanas Lopez, Hoang Dung Tran and Taylor T Johnson: Differential Algebraic Equations (DAEs) with Varying Index</td></tr>
<tr><td class="program-time">16:15</td><td class="program-topic">Hoang Dung Tran, Tianshu Bao and Taylor T. Johnson: Discrete-Space Analysis of Partial Differential Equations</td></tr>
<tr><td class="program-time">16:30</td><td class="program-topic">Nikolaos Kekatos, Daniel Hess and Goran Frehse: Lane change maneuver for autonomous vehicles</td></tr>
<tr><td class="program-time">16:45</td><td class="program-topic">Nathalie Cauchi and Alessandro Abate: A modular library of stochastic models from building automation systems</td></tr>
</tbody></table></div>
<h3 class="file-year">Benchmarks</h3>
<ul class="file-list">
<li class="file-item"><span class="file-title">Benchmark package 2</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH18_Attachment_2zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark package 3</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH18_Attachment_3zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark package 4</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH18_Attachment_4zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark package 6</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH18_Attachment_6zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark package 7</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH18_Attachment_7zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark package 8</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH18_Attachment_8zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark package 9</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH18_Attachment_9zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
</ul>
<h3 class="file-year">Tool Presentations</h3>
<ul class="file-list">
<li class="file-item"><span class="file-title">Tool presentation 1</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/tool-presentations/ARCH18_Attachment_1zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
</ul>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="https://easychair.org/publications/volume/ARCH18" target="_blank" rel="noopener">EPiC proceedings volume</a></div><div><a href="https://gitlab.com/goranf/ARCH-COMP/-/tree/master/2018" target="_blank" rel="noopener">Repeatability packages</a></div></div>
</section>
<section class="edition" id="y2017" data-year="2017" hidden>
<div class="edition-head"><h2 class="subpage-title">ARCH 2017</h2><p class="edition-when">April 17, 2017 · Pittsburgh, USA</p></div>
<h3 class="file-year">Program</h3>
<p class="section-text">09:00-10:30 Invited Talk and Benchmarks I</p>
<div class="table-wrap"><table class="program-table"><tbody>
<tr><td class="program-time">09:00</td><td class="program-topic">Invited Talk: Sebastian Scherer Challenges for Safe Autonomous Flight</td></tr>
<tr><td class="program-time">10:00</td><td class="program-topic">Daniele Ioli, Alessandro Falsone, Marianne Hartung, Axel Busboom and Maria Prandini: A smart-grid energy management problem for data-driven design with probabilistic reachability guarantees</td></tr>
<tr><td class="program-time">10:15</td><td class="program-topic">Nicole Chan and Sayan Mitra: Verifying safety of an autonomous spacecraft rendezvous mission</td></tr>
<tr><td class="program-time">10:30-11:00</td><td class="program-topic">Coffee break</td></tr>
<tr><td class="program-time">11:00-12:00</td><td class="program-topic">Benchmarks II</td></tr>
<tr><td class="program-time">11:00</td><td class="program-topic">Hoang-Dung Tran, Luan Viet Nguyen, Weiming Xiang and Taylor Johnson: Distributed Autonomous Systems</td></tr>
<tr><td class="program-time">11:15</td><td class="program-topic">Alena Rodionova, Matthew O'Kelly, Houssam Abbas, Vincent Pacelli and Rahul Mangharam: An Autonomous Vehicle Control Stack</td></tr>
<tr><td class="program-time">11:30</td><td class="program-topic">Omar Beg, Ali Davoudi and Taylor T Johnson: Reachability Analysis of Transformer-Isolated DC-DC Converters</td></tr>
<tr><td class="program-time">11:45</td><td class="program-topic">Andreas Muller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and Andre Platzer: A Benchmark for Component-based Hybrid Systems Safety Verification</td></tr>
<tr><td class="program-time">12:00-13:30</td><td class="program-topic">Lunch</td></tr>
<tr><td class="program-time">13:30-14:50</td><td class="program-topic">Contributed Papers</td></tr>
<tr><td class="program-time">13:30</td><td class="program-topic">Xin Chen, Souradeep Dutta and Sriram Sankaranarayanan: Formal Verification of a Multi-Basal Insulin Infusion Control Model</td></tr>
<tr><td class="program-time">13:50</td><td class="program-topic">Christof Budnik, Sebastian Eckl and Marco Gario: A Hybrid Testbed for Verification of Cyber-physical Production Systems</td></tr>
<tr><td class="program-time">14:10</td><td class="program-topic">Nikolaos Kekatos, Marcelo Forets and Goran Frehse: Modeling the Wind Turbine Benchmark with PWA Hybrid Automata</td></tr>
<tr><td class="program-time">14:30</td><td class="program-topic">Stanley Bak and Parasara Sridhar Duggirala: Direct Verification of Linear Systems with over 10000 Dimensions</td></tr>
<tr><td class="program-time">14:50-15:30</td><td class="program-topic">Coffee break</td></tr>
<tr><td class="program-time">15:30-17:00</td><td class="program-topic">ARCH Competition Results and Discussion</td></tr>
<tr><td class="program-time">15:30</td><td class="program-topic">Affine and piecewise affine dynamics (lead: Matthias Althoff)</td></tr>
<tr><td class="program-time">15:45</td><td class="program-topic">Nonlinear dynamics (lead: Xin Chen)</td></tr>
<tr><td class="program-time">16:00</td><td class="program-topic">Piecewise constant dynamics (lead: Goran Frehse)</td></tr>
<tr><td class="program-time">16:15</td><td class="program-topic">Bounded model checking (lead: Lei Bu)</td></tr>
<tr><td class="program-time">16:30</td><td class="program-topic">Falsification and parameter-centric problems (lead: Georgios Fainekos)</td></tr>
</tbody></table></div>
<h3 class="file-year">Benchmarks</h3>
<ul class="file-list">
<li class="file-item"><span class="file-title">Benchmark package 1</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH17_Attachment_1zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark package 2</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH17_Attachment_2zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark package 3</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH17_Attachment_3zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark package 6</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH17_Attachment_6zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark package 7</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH17_Attachment_7zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
</ul>
<h3 class="file-year">Experience Reports</h3>
<ul class="file-list">
<li class="file-item"><span class="file-title">Experience report 9</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/experience-reports/ARCH17_Attachment_9zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Experience report 11</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/experience-reports/ARCH17_Attachment_11zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
</ul>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="https://easychair.org/publications/volume/ARCH17" target="_blank" rel="noopener">EPiC proceedings volume</a></div><div><a href="https://gitlab.com/goranf/ARCH-COMP/-/tree/master/2017" target="_blank" rel="noopener">Repeatability packages</a></div></div>
</section>
<section class="edition" id="y2016" data-year="2016" hidden>
<div class="edition-head"><h2 class="subpage-title">ARCH 2016 <span class="edition-badge muted-badge">Pre-competition</span></h2><p class="edition-when">April 11, 2016 · Vienna, Austria</p></div>
<h3 class="file-year">Program</h3>
<p class="section-text">Pdf version of the <a href="https://cps-vo.org/node/25354" target="_blank" rel="noopener">program</a>.</p>
<div class="table-wrap"><table class="program-table"><tbody>
<tr><td class="program-time">08:00</td><td class="program-topic">Registration</td></tr>
<tr><td class="program-time">09:00-10:25</td><td class="program-topic">Invited Talk and Benchmarks I Invited Talk: Dirk Beyer: Reliable and Reproducible Competition Results Houssam Abbas, Kuk Jin Jang and Rahul Mangharam: Nonlinear Hybrid Automata Model of Excitable Cardiac Tissue Sidharta Andalam, Avinash Malik, Partha Roop and Mark Trew: Hybrid automata model of the heart for formal verification of pacemakers</td></tr>
<tr><td class="program-time">10:25-11:00</td><td class="program-topic">Coffee break</td></tr>
<tr><td class="program-time">11:00-12:20</td><td class="program-topic">Benchmarks II Scott Livingston and Vasumathi Raman: Chains of Integrators as a Benchmark for Scalability of Hybrid Control Synthesis Andrew Sogokon, Taylor T Johnson and Khalil Ghorbal: Benchmarks for Non-linear Continuous System Safety Verification Omar Beg, Ali Davoudi and Taylor T Johnson: Formal Verification of Charge Pump Phase-Locked Loop and Full Wave Rectifier Through Reachability Analysis Simone Schuler, Fabiano Daher Adegas and Adolfo Anta: Hybrid modelling of a wind turbine</td></tr>
<tr><td class="program-time">12:20-14:00</td><td class="program-topic">Lunch</td></tr>
<tr><td class="program-time">14:00-15:20</td><td class="program-topic">Benchmarks III and Tools I Sergiy Bogomolov, Christian Herrera and Wilfried Steiner: Benchmark for Verification of Fault-Tolerant Clock Synchronization Algorithms Hoang-Dung Tran, Luan Viet Nguyen and Taylor T Johnson: Large-Scale Linear Systems from Order-Reduction Stanley Bak, Sergiy Bogomolov and Christian Schilling: High-level Hybrid Systems Analysis with Hypy Ibtissem Ben Makhlouf, Norman Hansen and Stefan Kowalewski: HyReach: A Reachability Tool for Linear Hybrid Systems Based on Support Functions</td></tr>
<tr><td class="program-time">15:20-16:00</td><td class="program-topic">Coffee break</td></tr>
<tr><td class="program-time">16:00-17:20</td><td class="program-topic">Tools II Axel Busboom, Simone Schuler and Alexander Walsch: FormalSpec - semi-automatic formalization of system requirements for formal verification Dalibor Drzajic, Nikolaos Kariotoglou, Maryam Kamgarpour and John Lygeros: A Semidefinite Programming Approach to Control Synthesis for Stochastic Reach-Avoid Problems Heinz Riener, Robert Koenighofer, Goerschwin Fey and Roderick Bloem: SMT-Based CPS Parameter Synthesis and Repair Matthias Althoff and Dmitry Grebenyuk Implementation of Interval Arithmetic in CORA 2016</td></tr>
</tbody></table></div>
<h3 class="file-year">Benchmarks</h3>
<ul class="file-list">
<li class="file-item"><span class="file-title">Hybrid automata model of the heart for formal verification of pacemakers</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_paper_1pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_Attachment_1zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Hybrid modelling of a wind turbine</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_paper_3pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_Attachment_3zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Formal Verification of Charge Pump Phase-Locked Loop and Full Wave Rectifier Through Reachability Analysis</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_paper_9pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_Attachment_9zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Nonlinear Hybrid Automata Model of Excitable Cardiac Tissue</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_paper_10pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_Attachment_10zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmarks for Non-linear Continuous System Safety Verification</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_paper_12pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_Attachment_12zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Chains of Integrators as a Benchmark for Scalability of Hybrid Control Synthesis</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_paper_13pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_Attachment_13tgz.tar.gz" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Large-Scale Linear Systems from Order-Reduction</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_paper_15pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_Attachment_15zip.zip" target="_blank" rel="noopener">Models (ZIP)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_Attachment_15_update_27March2017zip.zip" target="_blank" rel="noopener">Update 27March2017 (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark for Verification of Fault-Tolerant Clock Synchronization Algorithms</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_paper_16pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH16_Attachment_16zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
</ul>
<h3 class="file-year">Tool Presentations</h3>
<ul class="file-list">
<li class="file-item"><span class="file-title">HyReach: A Reachability Tool for Linear Hybrid Systems Based on Support Functions</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/tool-presentations/ARCH16_paper_2pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/tool-presentations/ARCH16_Attachment_2zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">High-level Hybrid Systems Analysis with Hypy</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/tool-presentations/ARCH16_paper_4pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a></span></li>
<li class="file-item"><span class="file-title">Implementation of Interval Arithmetic in CORA 2016</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/tool-presentations/ARCH16_paper_5pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a></span></li>
<li class="file-item"><span class="file-title">SMT-Based CPS Parameter Synthesis and Repair</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/tool-presentations/ARCH16_paper_7pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/tool-presentations/ARCH16_Attachment_7tgz.tar.gz" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">A Semidefinite Programming Approach to Control Synthesis for Stochastic Reach-Avoid Problems</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/tool-presentations/ARCH16_paper_14pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a></span></li>
<li class="file-item"><span class="file-title">FormalSpec - semi-automatic formalization of system requirements for formal verification</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/tool-presentations/ARCH16_paper_17pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/tool-presentations/ARCH16_Attachment_17zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
</ul>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="https://easychair.org/publications/volume/ARCH16" target="_blank" rel="noopener">EPiC proceedings volume</a></div></div>
</section>
<section class="edition" id="y2015" data-year="2015" hidden>
<div class="edition-head"><h2 class="subpage-title">ARCH 2015 <span class="edition-badge muted-badge">Pre-competition</span></h2><p class="edition-when">April 13, 2015 · Seattle, USA</p></div>
<h3 class="file-year">Program</h3>
<div class="table-wrap"><table class="program-table"><tbody>
<tr><td class="program-time">08:00</td><td class="program-topic">Registration</td></tr>
<tr><td class="program-time">08:30-10:00</td><td class="program-topic">Invited Talk & Tool Presentation Invited Talk: Jay Abraham (Mathworks) - Verification and test of embedded software with model-based design Chuchu Fan, Parasara Sridhar Duggirala, Sayan Mitra and Mahesh Viswanathan: Progress on Powertrain Verification Challenge with C2E2</td></tr>
<tr><td class="program-time">10:00-10:30</td><td class="program-topic">Coffee break</td></tr>
<tr><td class="program-time">10:30-12:00</td><td class="program-topic">Tools Matthias Althoff: An Introduction to CORA 2015 Fabian Immler: Isabelle/HOL for Reachability Analysis of Continuous Systems Stefano Minopoli and Goran Frehse: Running SpaceEx on the ARCH14 Benchmarks Xin Chen, Sriram Sankaranarayanan and Erika Abraham: Flow* 1.2: More Effective to Play with Hybrid Systems</td></tr>
<tr><td class="program-time">12:00-13:00</td><td class="program-topic">Lunch</td></tr>
<tr><td class="program-time">13:00-14:30</td><td class="program-topic">Tools & Experience Reports Alexandre Donze and Vasumathi Raman: BluSTL: Controller Synthesis from Signal Temporal Logic Specifications Kyungmin Bae, Soonho Kong and Sicun Gao: SMT Encoding of Hybrid Systems in dReal Thomas Strathmann and Jens Oehlerking: Verifying Properties of an Electro-Mechanical Braking System Hendrik Roehm, Rainer Gmehlich, Thomas Heinz, Jens Oehlerking and Matthias Woehrle: Industrial Examples of Formal Specifications for Test Case Generation</td></tr>
<tr><td class="program-time">14:30-15:00</td><td class="program-topic">Coffee break</td></tr>
<tr><td class="program-time">15:00-17:00</td><td class="program-topic">Benchmarks Luca Parolini, Simone Schuler and Adolfo Anta: An air brake model for trains Jyotirmoy Deshmukh, Hisahiro Ito, Xiaoqing Jin, James Kapinski, Ken Butts, Behzad Samadi and Kevin Walker: PWA Models of a Powertrain Control Benchmark Hoang-Dung Tran, Luan Viet Nguyen and Taylor T Johnson: A Nonlinear Reachability Analysis Test Set from Numerical Analysis A. E. C. Da Cunha: Quadrotor Attitude Control Stanley Bak, Sergiy Bogomolov, Marius Greitschus and Taylor T Johnson: Benchmark Generator for Stratified Controllers of Tank Networks</td></tr>
</tbody></table></div>
<h3 class="file-year">Benchmarks</h3>
<ul class="file-list">
<li class="file-item"><span class="file-title">Benchmark problem: an air brake model for trains</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH15_submission_1pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH15_attachment_1zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark: Quadrotor Attitude Control</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH15_submission_3pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH15_attachment_3zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark: Stratified Controllers of Tank Networks</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH15_submission_4pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH15_attachment_4zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmark: A Nonlinear Reachability Analysis Test Set from Numerical Analysis</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH15_submission_9pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/ARCH15_attachment_9zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
</ul>
<h3 class="file-year">Experience Reports</h3>
<ul class="file-list">
<li class="file-item"><span class="file-title">Experience Report: Verifying Properties of an Electro-Mechanical Braking System</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/experience-reports/ARCH15_submission_2pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/experience-reports/ARCH15_attachment_2zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Industrial Examples of Formal Specifications for Test Case Generation</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/experience-reports/ARCH15_submission_6pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a></span></li>
<li class="file-item"><span class="file-title">Optimizing Safe Control of a Networked Platoon of Trucks Using Reachability</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/experience-reports/ARCH15_submission_11pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a></span></li>
<li class="file-item"><span class="file-title">Piecewise-Affine Approximations for a Powertrain Control Verification Benchmark</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/experience-reports/ARCH15_submission_16pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/experience-reports/ARCH15_attachment_16zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
</ul>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="https://easychair.org/publications/volume/ARCH15" target="_blank" rel="noopener">EPiC proceedings volume</a></div></div>
</section>
<section class="edition" id="y2014" data-year="2014" hidden>
<div class="edition-head"><h2 class="subpage-title">ARCH 2014 <span class="edition-badge muted-badge">Pre-competition</span></h2><p class="edition-when">April 14, 2014 · Berlin, Germany</p></div>
<h3 class="file-year">Program</h3>
<div class="table-wrap"><table class="program-table"><tbody>
<tr><td class="program-time">08:00</td><td class="program-topic">Registration</td></tr>
<tr><td class="program-time">09:00-11:00</td><td class="program-topic">Invited Talk and Benchmark Presentations I Invited Talk: Bernard Dion (Esterel Technologies) - 15 years of Industry experience in developing and verifying critical systems Victor Gan, Guy A. Dumont and Ian M. Mitchell . Benchmark Problem: A PK/PD Model and Safety Constraints for Anesthesia Delivery Hongxu Chen , Sayan Mitra and Guangyu Tian. Motor-Transmission Drive System: a Benchmark Example for Safety Verification Bardh Hoxha, Houssam Abbas and Georgios Fainekos. Benchmarks for Temporal Logic Requirements for Automotive Systems</td></tr>
<tr><td class="program-time">11:00-11:30</td><td class="program-topic">Coffee break</td></tr>
<tr><td class="program-time">11:30-13:00</td><td class="program-topic">Benchmark Presentations II Thomas Heinz , Jens Oehlerking and Matthias Woehrle. Benchmark: Reachability on a model with holes Ibtissem Ben Makhlouf . WLAN Cooperative Platoon of Vehicles for Testing Methods and Verification Tools Luan Nguyen and Taylor T Johnson . Benchmark: DC-to-DC Switched-Mode Power Converters (Buck Converters, Boost Converters, and Buck-Boost Converters) Xiaoqing Jin, Jyotirmoy Deshmukh , James Kapinski, Koichi Ueda and Ken Butts. Benchmarks for Model Transformations and Conformance Checking</td></tr>
<tr><td class="program-time">13:00-14:00</td><td class="program-topic">Lunch</td></tr>
<tr><td class="program-time">14:00-16:00</td><td class="program-topic">Experience Reports and Tool Presentations Olivier Bouissou, Alexandre Chapoutot and Samuel Mimram. Simulation and Verification of Hybrid Systems using HySon Eike Moehlmann, Willem Hagemann and Astrid Rakow . Verifying a PI Controller using SoapBox and Stabhyli Bardh Hoxha, Houssam Abbas and Georgios Fainekos. Using S-TaLiRo on Industrial Size Automotive Models</td></tr>
<tr><td class="program-time">16:00-16:30</td><td class="program-topic">Coffee break</td></tr>
<tr><td class="program-time">16:30-18:00</td><td class="program-topic">Benchmark Repository and Panel Discussion Presentation and Discussion of the Online Benchmark Repository Panel Discussion: How to certify cyber-physical systems? Perspectives from industry and academia</td></tr>
</tbody></table></div>
<h3 class="file-year">Benchmarks</h3>
<ul class="file-list">
<li class="file-item"><span class="file-title">Reachability on a model with holes</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_submission_3pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_attachment_3zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmarks for Model Transformations and Conformance Checking</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_submission_7pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_attachment_7zip.zip" target="_blank" rel="noopener">Models (ZIP)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_attachment_7_update_18Dec2014zip.zip" target="_blank" rel="noopener">Update 18Dec2014 (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Motor-Transmission Drive System: a Benchmark Example for Safety Verification</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_submission_8pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_attachment_8_mesh_model_update06April2017zip.zip" target="_blank" rel="noopener">Mesh model (ZIP)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_attachment_8_mesh_modelzip.zip" target="_blank" rel="noopener">Mesh model (ZIP)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_attachment_8zip.zip" target="_blank" rel="noopener">Models (ZIP)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_attachment_8_update06April2017zip.zip" target="_blank" rel="noopener">Update 06April2017 (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">A PK/PD Model and Safety Constraints for Anesthesia Delivery</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_submission_10pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_attachment_10zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">DC-to-DC Switched-Mode Power Converters (Buck Converters, Boost Converters, and Buck-Boost Converters)</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_submission_12pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_attachment_12zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Flight Envelope Protection in Autonomous Quadrotors</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_submission_13pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_attachment_13zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Networked Cooperative Platoon of Vehicles for Testing Methods and Verification Tools</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_submission_14pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a> <a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_attachment_14zip.zip" target="_blank" rel="noopener">Models (ZIP)</a></span></li>
<li class="file-item"><span class="file-title">Benchmarks for Temporal Logic Requirements for Automotive Systems</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/benchmarks/arch14_submission_15pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a></span></li>
</ul>
<h3 class="file-year">Experience Reports</h3>
<ul class="file-list">
<li class="file-item"><span class="file-title">Computing Probability Distributions Over a Hybrid State</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/experience-reports/arch14_submission_9pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a></span></li>
<li class="file-item"><span class="file-title">Verifying a PI Controller using SoapBox and Stabhyli</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/experience-reports/arch14_submission_11pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a></span></li>
<li class="file-item"><span class="file-title">Using S-TaLiRo on Industrial Size Automotive</span><span class="file-links"><a href="https://media.githubusercontent.com/media/ARCH-COMP/arch-comp.github.io/main/files/experience-reports/arch14_submission_16pdf.pdf" target="_blank" rel="noopener">Paper (PDF)</a></span></li>
</ul>
<h3 class="file-year">Proceedings & Repeatability</h3>
<div class="facts"><div><a href="https://easychair.org/publications/volume/ARCH15" target="_blank" rel="noopener">EPiC proceedings volume</a></div></div>
</section>
<div class="publications-section" id="publications" style="margin-top:3.5rem;">
<h2 style="border:none; margin-bottom:1.25rem;">Publications</h2>
<div class="overview-paper">
<h4>Overview Paper</h4>
<p class="paper-citation">
A. Abate, M. Althoff, L. Bu, G. Ernst, G. Frehse, L. Geretti, T. T. Johnson, C. Menghi,
S. Mitsch, S. Schupp, and S. Soudjani,
"<a href="https://doi.org/10.1007/978-3-031-67695-6_1" target="_blank" rel="noopener">The ARCH-COMP Friendly Verification Competition for Continuous and Hybrid Systems</a>,"
in <em>TOOLympics Challenge 2023</em>, LNCS, Springer, pp. 1–37, 2023.
</p>
</div>
<div class="bibtex-section">
<h4>BibTeX <button class="copy-bibtex-btn" onclick="copyBibtex()">Copy</button></h4>
<pre class="bibtex-code" id="bibtex-content">@inproceedings{abate2023archcomp_overview,
title = {The {ARCH-COMP} Friendly Verification Competition for Continuous and Hybrid Systems},
author = {Abate, Alessandro and Althoff, Matthias and Bu, Lei and Ernst, Gidon and Frehse, Goran and Geretti, Luca and Johnson, Taylor T. and Menghi, Claudio and Mitsch, Stefan and Schupp, Stefan and Soudjani, Sadegh},
booktitle = {TOOLympics Challenge 2023},
series = {Lecture Notes in Computer Science},
pages = {1--37},
year = {2023},
publisher = {Springer},
doi = {10.1007/978-3-031-67695-6_1}
}</pre>
</div>
</div>
</div>
</main>
<footer class="footer">
<div class="container">
<div class="footer-content">
<div class="footer-info">
<h3>ARCH-COMP</h3>
<p>Applied Verification of Continuous and Hybrid Systems</p>
</div>
<nav class="footer-links" aria-label="Footer">
<a href="index.html#about">About</a>
<a href="participate.html">Participate</a>
<a href="editions.html">Editions</a>
<a href="https://github.com/ARCH-COMP" target="_blank" rel="noopener">GitHub</a>
</nav>
</div>
<div class="footer-bottom">
<p>© 2027 ARCH-COMP. Content licensed under the MIT License.</p>
</div>
</div>
</footer>
<script>
(function () {
var sel = document.getElementById('year-select');
var editions = Array.prototype.slice.call(document.querySelectorAll('.edition'));
function show(year) {
editions.forEach(function (s) { s.hidden = (s.dataset.year !== year); });
if (sel.value !== year) sel.value = year;
}
sel.addEventListener('change', function () {
show(sel.value);
history.replaceState(null, '', '#' + sel.value);
});
var initial = (location.hash || '').replace('#', '');
if (initial && editions.some(function (s) { return s.dataset.year === initial; })) {
show(initial);
}
})();
</script>
<script src="script.js"></script>
</body>
</html>