Sylvain Schmitz
Assistant professor
Algorithmic Applications of wqos
I've been busy these last few years trying to get a clear
picture of the complexity of problems that arise from the use of
wellquasiorders and wellstructured transition systems. Here
is some of the material I coauthored on the subject:
Research
 Keywords
 Verification, infinite systems, well quasi orders, formal languages, parsing, computational linguistics
• 
Th. Colcombet, M. Jurdziński, R. Lazić and S. Schmitz. Perfect Half Space Games. In LICS'17, pages 111. IEEE Press, June 2017. ( Web page  BibTeX )

• 
B. Bérard, S. Haar, S. Schmitz and S. Schwoon. The Complexity of Diagnosability and Opacity Verification for Petri
Nets. In PETRI NETS'17, LNCS 10258, pages 200220. Springer, June 2017. ( Web page  BibTeX )

• 
J. GoubaultLarrecq and S. Schmitz. Deciding Piecewise Testable Separability for Regular Tree Languages. In ICALP'16, Leibniz International Proceedings in Informatics 55, pages 97:197:15. LeibnizZentrum für Informatik, July 2016. ( Web page  BibTeX )

• 
R. Lazić and S. Schmitz. The Complexity of Coverability in νPetri Nets. In LICS'16, pages 467476. ACM Press, July 2016. ( Web page  BibTeX )

• 
D. Baelde, S. Lunel and S. Schmitz. A Sequent Calculus for a Modal Logic on Finite Data Trees. In CSL'16, Leibniz International Proceedings in Informatics 62, pages 32:132:16. LeibnizZentrum für Informatik, September 2016. ( Web page  BibTeX )

Full BibTeX
More publications...
 Workshop on Separability Problems, 12:15am, July 14th, 2017, University of Warsaw, Warsaw, Poland
 In this invited talk, I presented the wqo viewpoint on piecewisetestable separability problems, based on the ICALP'16 paper with J. GoubaultLarrecq.
 Gregynog 71717, 10am, July 4th, 2017, Gregynog, Wales

I presented a dual approach to the backward coverability algorithm in wellstructured transition systems, using ideal decompositions of downwardsclosed sets, and allowing a fine complexity analysis. This is based on a joint paper with R. Lazić.
 LICS 2017, 11:20am, June 23rd, room M1.01, Reykjavik University, Iceland
 I presented the paper Perfect Half Space Games written jointly with Th. Colcombet, M. Jurdziński, and R. Lazić. Here are the slides.
 Automata Theory Seminar, 2:15pm, June 7th, 2017, room 5870, University of Warsaw, Poland
 I presented an approach to solving separability by piecewisetestable sets using ideal decompositions. The talk was based on a joint paper with J. GoubaultLarrecq published at ICALP last year.
 Automata Theory Seminar, 2:15pm, May 24th, 2017, room 5870, University of Warsaw, Poland
 I presented an approach to computing downwardclosures using ideal decompositions. The talk was based on a joint paper with J. GoubaultLarrecq published at ICALP last year.
 LSV's 20th Anniversary, 3:15pm, May 12th, 2017, ENS Cachan, Cachan,
France.

A typical application of wellquasiorders is program termination, which can be shown by mapping any execution sequence of a program to a socalled bad sequence of longer or equal length: as bad sequences are finite, so are executions, and this shows that the program terminates. I showed how such termination proofs can be instrumented to yield complexity upper bounds, by considering the example of the decomposition algorithm for reachability in vector addition systems. Here are the slides.
More talks...
Other activities
 Steering committee of GTVerif.
 PC member for conferences LICS'18, Petri nets'17, STACS'17, and workshops RP'15, RP'12, CSLP'12, LDTA'12, LDTA'11, TAG+10, TAG+9;
 organizing committees of Highlights 2014 (cochair), GTVérif 2014, GTVérif 2013 (cochair), CIAA'05.