PageSourceSearch

https://p-offtermatt.github.io/publications/

html p-offtermatt.github.io collected 2026-10-03 09:43:53 UTC 19,368 bytes, 808 lines download raw bytes

1<!DOCTYPE html>
2<html>
3
4  <head>
5    <meta charset="utf-8">
6<meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
7<meta http-equiv="X-UA-Compatible" content="IE=edge">
8
9<title>Philip Offtermatt | Publications</title>
10<meta name="description" content="I am a Ph.D. student at the Université de Sherbrooke  and the Max Planck Institute for Software Systems  in Saarbrücken.
11">
12
13<!-- Bootstrap & MDB -->
14<link href="https://stackpath.bootstrapcdn.com/bootstrap/4.4.1/css/bootstrap.min.css" rel="stylesheet" integrity="sha384-Vkoo8x4CGsO3+Hhxv8T/Q5PaXtkKtu6ug5TOeNV6gBiFeWPGFN9MuhOf23Q9Ifjh" crossorigin="anonymous">
15<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/mdbootstrap/4.17.0/css/mdb.min.css" integrity="sha256-/SwJ2GDcEt5382i8zqDwl36VJGECxEoIcBIuoLmLR4g=" crossorigin="anonymous" />
16
17<!-- Fonts & Icons -->
18<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/5.13.0/css/all.min.css"  integrity="sha256-h20CPZ0QyXlBuAw7A+KluUYx/3pK+c7lYEpqLTlxjYQ=" crossorigin="anonymous">
19<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/academicons/1.8.6/css/academicons.min.css" integrity="sha256-uFVgMKfistnJAfoCUQigIl+JfUaP47GrRKjf6CTPVmw=" crossorigin="anonymous">
20<link rel="stylesheet" type="text/css" href="https://fonts.googleapis.com/css?family=Roboto:300,400,500,700|Roboto+Slab:100,300,400,500,700|Material+Icons">
21
22<!-- Styles -->
23<link rel="shortcut icon" href="/assets/img/favicon.ico">
24<link rel="stylesheet" href="/assets/css/main.css">
25
26<link rel="canonical" href="/publications/">
27
28<!-- Open Graph -->
29
30
31  </head>
32
33  <body class="fixed-top-nav ">
34
35    <!-- Header -->
36
37    <header>
38
39    <!-- Nav Bar -->
40    <nav id="navbar" class="navbar navbar-light bg-white navbar-expand-sm fixed-top">
41    <div class="container">
42      
43      
44      
45      
46      
47      <a class="navbar-brand title font-weight-lighter" href="/">
48       <span class="font-weight-bold">Philip</span>   Offtermatt
49      </a>
50      
51      <!-- Navbar Toogle -->
52      <button class="navbar-toggler collapsed ml-auto" type="button" data-toggle="collapse" data-target="#navbarNav" aria-controls="navbarNav" aria-expanded="false" aria-label="Toggle navigation">
53        <span class="sr-only">Toggle navigation</span>
54        <span class="icon-bar top-bar"></span>
55        <span class="icon-bar middle-bar"></span>
56        <span class="icon-bar bottom-bar"></span>
57      </button>
58      <div class="collapse navbar-collapse text-right" id="navbarNav">
59        <ul class="navbar-nav ml-auto flex-nowrap">
60          <!-- About -->
61          <li class="nav-item ">
62            <a class="nav-link" href="/">
63              About
64              
65            </a>
66          </li>
67          
68          <!-- Other pages -->
69          
70          
71          
72          
73          
74          
75          
76          
77          
78          <li class="nav-item ">
79              <a class="nav-link" href="/assets/pdf/CV.pdf">
80                CV
81                
82              </a>
83          </li>
84          
85          
86          
87          <li class="nav-item ">
88              <a class="nav-link" href="/projects/">
89                Projects
90                
91              </a>
92          </li>
93          
94          
95          
96          <li class="nav-item active">
97              <a class="nav-link" href="/publications/">
98                Publications
99                
100                <span class="sr-only">(current)</span>
101                
102              </a>
103          </li>
104          
105          
106          
107          <li class="nav-item ">
108              <a class="nav-link" href="/talks/">
109                Talks
110                
111              </a>
112          </li>
113          
114          
115        </ul>
116      </div>
117    </div>
118  </nav>
119
120</header>
121
122
123    <!-- Content -->
124
125    <div class="container mt-5">
126      <div class="post">
127
128  <header class="post-header">
129    <h1 class="post-title">Publications</h1>
130    <p class="post-description">A list of my publications.</p>
131  </header>
132
133  <article>
134    <div class="publications">
135
136
137  <h2 class="year">2022</h2>
138  <ol class="bibliography"><li><div class="row">
139  <div class="col-sm-2 abbr">
140  
141    
142    <abbr class="badge">Accepted at TOCL</abbr>
143    
144  
145  </div>
146
147  <div id="coca_journal" class="col-sm-8">
148    
149      <span class="title">Continuous One-Counter Automata</span>
150      <span class="author">
151        
152          
153            
154              
155                
156                  <a href="http://info.usherbrooke.ca/mblondin/" target="_blank">Blondin, Michael</a>,
157                
158              
159            
160          
161        
162          
163            
164              
165                
166                  <a href="http://timleys.be/" target="_blank">Leys, Tim</a>,
167                
168              
169            
170          
171        
172          
173            
174              
175                
176                  <a href="https://fmazowiecki.github.io/" target="_blank">Mazowiecki, Filip</a>,
177                
178              
179            
180          
181        
182          
183            
184              
185                <em>Offtermatt, Philip</em>,
186              
187            
188          
189        
190          
191            
192              
193                
194                  and Pérez, Guillermo A.
195                
196              
197            
198          
199        
200      </span>
201
202      <span class="periodical">
203      
204        <em></em>
205      
206      
207        2022
208      
209      </span>
210    
211
212    <span class="links">
213    
214      [<a class="abstract">Abs</a>]
215    
216    
217    
218    
219    
220    
221    
222    
223    </span>
224
225    <!-- Hidden abstract block -->
226    
227    <span class="abstract hidden">
228      <p>We study the reachability problem for continuous one-counter automata, COCA for short. In such automata,
229transitions are guarded by upper and lower bound tests against the counter value. Additionally, the counter
230updates associated with taking transitions can be (non-deterministically) scaled down by a nonzero factor
231between zero and one. Our three main results are as follows: (1) We prove that the reachability problem for
232COCA with global upper and lower bound tests is in NC2; (2) that, in general, the problem is decidable in
233polynomial time; and (3) that it is NP-complete for COCA with parametric counter updates and bound tests.</p>
234    </span>
235    
236  </div>
237</div>
238</li>
239<li><div class="row">
240  <div class="col-sm-2 abbr">
241  
242    
243    <abbr class="badge">Accepted at CAV</abbr>
244    
245  
246  </div>
247
248  <div id="https://arxiv.org/abs/2206.02606" class="col-sm-8">
249    
250      <span class="title">Verifying generalised and structural soundness of workflow nets via relaxations</span>
251      <span class="author">
252        
253          
254            
255              
256                
257                  <a href="http://info.usherbrooke.ca/mblondin/" target="_blank">Blondin, Michael</a>,
258                
259              
260            
261          
262        
263          
264            
265              
266                
267                  <a href="https://fmazowiecki.github.io/" target="_blank">Mazowiecki, Filip</a>,
268                
269              
270            
271          
272        
273          
274            
275              
276                and <em>Offtermatt, Philip</em>
277              
278            
279          
280        
281      </span>
282
283      <span class="periodical">
284      
285      
286        2022
287      
288      </span>
289    
290
291    <span class="links">
292    
293    
294    
295      [<a href="https://arxiv.org/abs/2206.02606" target="_blank">HTML</a>]
296    
297    
298    
299    
300    
301    
302    </span>
303
304    <!-- Hidden abstract block -->
305    
306  </div>
307</div>
308</li>
309<li><div class="row">
310  <div class="col-sm-2 abbr">
311  
312    
313    <abbr class="badge">Accepted at LICS</abbr>
314    
315  
316  </div>
317
318  <div id="https://doi.org/10.48550/arxiv.2201.05588" class="col-sm-8">
319    
320      <span class="title">The complexity of soundness in workflow nets</span>
321      <span class="author">
322        
323          
324            
325              
326                
327                  <a href="http://info.usherbrooke.ca/mblondin/" target="_blank">Blondin, Michael</a>,
328                
329              
330            
331          
332        
333          
334            
335              
336                
337                  <a href="https://fmazowiecki.github.io/" target="_blank">Mazowiecki, Filip</a>,
338                
339              
340            
341          
342        
343          
344            
345              
346                and <em>Offtermatt, Philip</em>
347              
348            
349          
350        
351      </span>
352
353      <span class="periodical">
354      
355      
356        2022
357      
358      </span>
359    
360
361    <span class="links">
362    
363    
364    
365      [<a href="https://arxiv.org/abs/2201.05588" target="_blank">HTML</a>]
366    
367    
368    
369    
370    
371    
372    </span>
373
374    <!-- Hidden abstract block -->
375    
376  </div>
377</div>
378</li></ol>
379
380  <h2 class="year">2021</h2>
381  <ol class="bibliography"><li><div class="row">
382  <div class="col-sm-2 abbr">
383  
384    
385    <abbr class="badge">LICS</abbr>
386    
387  
388  </div>
389
390  <div id="blondin2021continuous" class="col-sm-8">
391    
392      <span class="title">Continuous One-Counter Automata</span>
393      <span class="author">
394        
395          
396            
397              
398                
399                  <a href="http://info.usherbrooke.ca/mblondin/" target="_blank">Blondin, Michael</a>,
400                
401              
402            
403          
404        
405          
406            
407              
408                
409                  <a href="http://timleys.be/" target="_blank">Leys, Tim</a>,
410                
411              
412            
413          
414        
415          
416            
417              
418                
419                  <a href="https://fmazowiecki.github.io/" target="_blank">Mazowiecki, Filip</a>,
420                
421              
422            
423          
424        
425          
426            
427              
428                <em>Offtermatt, Philip</em>,
429              
430            
431          
432        
433          
434            
435              
436                
437                  and Pérez, Guillermo A.
438                
439              
440            
441          
442        
443      </span>
444
445      <span class="periodical">
446      
447        <em>In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS
448               2021, Rome, Italy, June 29 - July 2, 2021</em>
449      
450      
451        2021
452      
453      </span>
454    
455
456    <span class="links">
457    
458      [<a class="abstract">Abs</a>]
459    
460    
461    
462      [<a href="https://ieeexplore.ieee.org/document/9470525" target="_blank">HTML</a>]
463    
464    
465    
466    
467    
468    
469    </span>
470
471    <!-- Hidden abstract block -->
472    
473    <span class="abstract hidden">
474      <p>We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper and lower bound tests against the counter value. Additionally, the counter updates associated with taking transitions can be (non-deterministically) scaled down by a nonzero factor between zero and one. Our three main results are as follows: (1) We prove that the reachability problem for COCA with global upper and lower bound tests is in NC2; (2) that, in general, the problem is decidable in polynomial time; and (3) that it is decidable in the polynomial hierarchy for COCA with parametric counter updates and bound tests.</p>
475    </span>
476    
477  </div>
478</div>
479</li>
480<li><div class="row">
481  <div class="col-sm-2 abbr">
482  
483    
484    <abbr class="badge">TACAS</abbr>
485    
486  
487  </div>
488
489  <div id="blondin2021directed" class="col-sm-8">
490    
491      <span class="title">Directed Reachability for Infinite-State Systems</span>
492      <span class="author">
493        
494          
495            
496              
497                
498                  <a href="http://info.usherbrooke.ca/mblondin/" target="_blank">Blondin, Michael</a>,
499                
500              
501            
502          
503        
504          
505            
506              
507                
508                  <a href="http://www.cs.ox.ac.uk/people/christoph.haase/home/" target="_blank">Haase, Christoph</a>,
509                
510              
511            
512          
513        
514          
515            
516              
517                and <em>Offtermatt, Philip</em>
518              
519            
520          
521        
522      </span>
523
524      <span class="periodical">
525      
526        <em>In International Conference on Tools and Algorithms for the Construction and Analysis of Systems</em>
527      
528      
529        2021
530      
531      </span>
532    
533
534    <span class="links">
535    
536      [<a class="abstract">Abs</a>]
537    
538    
539    
540      [<a href="https://link.springer.com/chapter/10.1007%2F978-3-030-72013-1_1" target="_blank">HTML</a>]
541    
542    
543    
544    
545    
546    
547    </span>
548
549    <!-- Hidden abstract block -->
550    
551    <span class="abstract hidden">
552      <p>Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi-deciding the reachability problem for Petri nets in practice. Our key insight is that computationally lightweight over-approximations of Petri nets can be used as distance oracles in classical graph exploration algorithms such as A* and greedy best-first search. We provide and evaluate a prototype implementation of our approach that outperforms existing state-of-the-art tools, sometimes by orders of magnitude, and which is also competitive with domain-specific tools on benchmarks coming from program synthesis and concurrent program analysis.</p>
553    </span>
554    
555  </div>
556</div>
557</li></ol>
558
559  <h2 class="year">2019</h2>
560  <ol class="bibliography"><li><div class="row">
561  <div class="col-sm-2 abbr">
562  
563    
564    <abbr class="badge">TACAS</abbr>
565    
566  
567  </div>
568
569  <div id="meyer2019computing" class="col-sm-8">
570    
571      <span class="title">Computing the expected execution time of probabilistic workflow nets</span>
572      <span class="author">
573        
574          
575            
576              
577                
578                  <a href="https://www7.in.tum.de/people/detail/index.php?id=people.detail&amp;arg=152" target="_blank">Meyer, Philipp J</a>,
579                
580              
581            
582          
583        
584          
585            
586              
587                
588                  <a href="https://www7.in.tum.de/~esparza/" target="_blank">Esparza, Javier</a>,
589                
590              
591            
592          
593        
594          
595            
596              
597                and <em>Offtermatt, Philip</em>
598              
599            
600          
601        
602      </span>
603
604      <span class="periodical">
605      
606        <em>In International Conference on Tools and Algorithms for the Construction and Analysis of Systems</em>
607      
608      
609        2019
610      
611      </span>
612    
613
614    <span class="links">
615    
616    
617    
618      [<a href="https://link.springer.com/chapter/10.1007/978-3-030-17465-1_9" target="_blank">HTML</a>]
619    
620    
621    
622    
623    
624    
625    </span>
626
627    <!-- Hidden abstract block -->
628    
629  </div>
630</div>
631</li>
632<li><div class="row">
633  <div class="col-sm-2 abbr">
634  
635    
636    <abbr class="badge">Thesis</abbr>
637    
638  
639  </div>
640
641  <div id="offtermatt2019approaching" class="col-sm-8">
642    
643      <span class="title">Approaching Safety for Parameterized Systems via View Abstraction</span>
644      <span class="author">
645        
646          
647            
648              <em>Offtermatt, Philip</em>
649            
650          
651        
652      </span>
653
654      <span class="periodical">
655      
656      
657        2019
658      
659      </span>
660    
661
662    <span class="links">
663    
664    
665    
666    
667      [<a href="/assets/pdf/MastersThesis.pdf" target="_blank">PDF</a>]
668    
669    
670    
671    
672    
673    </span>
674
675    <!-- Hidden abstract block -->
676    
677  </div>
678</div>
679</li></ol>
680
681  <h2 class="year">2017</h2>
682  <ol class="bibliography"><li><div class="row">
683  <div class="col-sm-2 abbr">
684  
685    
686    <abbr class="badge">Thesis</abbr>
687    
688  
689  </div>
690
691  <div id="offtermatt2017tool" class="col-sm-8">
692    
693      <span class="title">A Tool for Verification and Simulation of Population Protocols</span>
694      <span class="author">
695        
696          
697            
698              <em>Offtermatt, Philip</em>
699            
700          
701        
702      </span>
703
704      <span class="periodical">
705      
706      
707        2017
708      
709      </span>
710    
711
712    <span class="links">
713    
714    
715    
716    
717      [<a href="/assets/pdf/BachelorsThesis.pdf" target="_blank">PDF</a>]
718    
719    
720    
721    
722    
723    </span>
724
725    <!-- Hidden abstract block -->
726    
727  </div>
728</div>
729</li></ol>
730
731
732</div>
733
734  </article>
735
736</div>
737
738    </div>
739
740    <!-- Footer -->
741
742    
743<footer class="fixed-bottom">
744  <div class="container mt-0">
745    Powered by <a href="http://jekyllrb.com/" target="_blank">Jekyll</a> with <a href="https://github.com/alshedivat/al-folio">al-folio</a> theme. Hosted by <a href="https://pages.github.com/" target="_blank">GitHub Pages</a>.
746
747    
748    Last updated: November 14, 2022.
749    
750  </div>
751</footer>
752
753
754
755  </body>
756
757  <!-- Load Core and Bootstrap JS -->
758<script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
vendor: 1 bytes, line 758
758
759<script src="https://cdnjs.cloudflare.com/ajax/libs/popper.js/2.4.0/umd/popper.min.js" integrity="sha256-OH05DFHUWzr725HmuHo3pnuvUUn+TJuj8/Qz9xytFEw=" crossorigin="anonymous"></script>
vendor: 1 bytes, line 759
759
760<script src="https://stackpath.bootstrapcdn.com/bootstrap/4.4.1/js/bootstrap.min.js" integrity="sha384-wfSDF2E50Y2D1uUdj0O3uMBJnjuUD4Ih7YwaYd1iqfktj0Uod8GCExl3Og8ifwB6" crossorigin="anonymous"></script>
vendor: 1 bytes, line 760
760
761<script src="https://cdnjs.cloudflare.com/ajax/libs/mdbootstrap/4.17.0/js/mdb.min.js"  integrity="sha384-wfSDF2E50Y2D1uUdj0O3uMBJnjuUD4Ih7YwaYd1iqfktj0Uod8GCExl3Og8ifwB6" crossorigin="anonymous"></script>
761
762
763<!-- Load Common JS -->
764<script src="/assets/js/common.js"></script>
764
765
766<!-- Code Syntax Highlighting -->
767<link rel="stylesheet" href="https://gitcdn.link/repo/jwarby/jekyll-pygments-themes/master/github.css" />
768
769
770<!-- Load KaTeX -->
771<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/KaTeX/0.11.1/katex.min.css" integrity="sha256-V8SV2MO1FUb63Bwht5Wx9x6PVHNa02gv8BgH/uH3ung=" crossorigin="anonymous" />
772<script src="https://cdnjs.cloudflare.com/ajax/libs/KaTeX/0.11.1/katex.min.js" integrity="sha256-F/Xda58SPdcUCr+xhSGz9MA2zQBPb0ASEYKohl8UCHc=" crossorigin="anonymous"></script>
vendor: 1 bytes, line 772
772
773<script src="/assets/js/katex.js"></script>
773
774
775
776
777<!-- Load Mansory & imagesLoaded -->
778<script src="https://cdnjs.cloudflare.com/ajax/libs/masonry/4.2.2/masonry.pkgd.min.js" integrity="" crossorigin="anonymous"></script>
vendor: 1 bytes, line 778
778
779<script src="https://unpkg.com/imagesloaded@4/imagesloaded.pkgd.min.js"></script>
779
780
781<!-- Project Cards Layout -->
782<script type="text/javascript">
783  // Init Masonry
784  var $grid = $('.grid').masonry({
785    gutter: 10,
786    horizontalOrder: true,
787    itemSelector: '.grid-item',
788  });
789  // layout Masonry after each image loads
790  $grid.imagesLoaded().progress( function() {
791    $grid.masonry('layout');
792  });
793</script>
793
794
795
796
797<!-- Enable Tooltips -->
798<script type="text/javascript">
799$(function () {
800  $('[data-toggle="tooltip"]').tooltip()
801})
802</script>
802
803
804
805
806
807
808</html>

Line numbers count LF bytes from the start of the resource, as the search results do. Vendor segments are library code the classifier recognised; they are stored but not indexed. Bytes are shown as Latin1 characters, one per byte.