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. IEEE Press, June 2017. To appear. ( 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...
 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.
 Verification Seminar, 11am, November 2nd, 2016, Department of Computer Science, Oxford University, Oxford, UK
 I presented the paper The Complexity of Coverability in νPetri Nets written with R. Lazić. Here are the slides.
 Verification Seminar, 11am, October 24th, 2016, IRIF, Paris, France
 I presented the applications of ideals of wellquasiorders for the verification of vector addition systems, based on the papers Demystifying Reachability in Vector Addition Systems and Ideal Decompositions for Vector Addition Systems with J. Leroux. Here are the slides.
 Highlights 2016, 14:51pm, September 8th, 2016, Université libre de Bruxelles, Brussels, Belgium.
 I presented a joint work with R. Lazić on the complexity of coverability in νPetri nets, an extension of Petri nets with data management and creation capabilities. Here are the papaer and the slides.
 ICALP 2016, 11:45am, July 12th, 2016, Sapienza University, Rome, Italy.
 I presented the paper Deciding Piecewise Testable Separability for Regular Tree Languages written with J. GoubaultLarrecq. Here are the slides.
 LICS 2016, 16:11pm, July 6th, 2016, Columbia University, New York, USA.
 I presented the joint paper with R. Lazić on the complexity of coverability in νPetri nets, an extension of Petri nets with data management and creation capabilities. Here are the preprint and the slides.
More talks...
Other activities
 Steering committee of GTVerif.
 PC member for conferences 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.