Section: Dissemination

Teaching - Supervision - Juries

Teaching

The university employees of VeriDis have significant teaching obligations. We indicate the graduate courses they have been teaching this year.

• Dominique Méry gave courses in the Master program in Nancy on: formal system engineering, modeling and verification of systems, theoretical computer science, development of software systems, distributed algorithms.

• Marie Duflot-Kremer and Stephan Merz taught a course on algorithmic verification in the Master program in Nancy.

• Uwe Waldmann taught a course on Automated Reasoning at Saarland University.

• Christoph Weidenbach gave a course on Automated Reasoning II and lectured within the series “Perspektiven der Informatik” at Saarland University.

Supervision

• PhD: Henri Debrat, Certification formelle de la correction d'algorithmes de Consensus, Université de Lorraine. Supervised by Bernadette Charron-Bost and Stephan Merz, defended on December 6, 2013.

• PhD: Tianxiang Lu, Formal Verification of the Pastry Protocol, Université de Lorraine and Universität des Saarlandes. Supervised by Stephan Merz and Christoph Weidenbach, defended on November 27, 2013.

• PhD in progress: Manamiary Andriamiarina, Refinement Techniques for Distributed Algorithms, Université de Lorraine. Supervised by Dominique Méry, since 10/2010.

• PhD in progress: Noran Azmy, On the Automation of Proofs in TLAPS, Saarland University. Supervised by Christoph Weidenbach, since 11/2012.

• PhD in progress: Haniel Barbosa, Refutational Completeness in Satisfiability Modulo Theories, Université de Lorraine. Supervised by Pascal Fontaine and Stephan Merz, since 12/2013.

• PhD in progress: Marek Košta, Computational Logic, Universität des Saarlandes. Supervised by Thomas Sturm, since 11/2011.

• PhD in progress: Hernán Vanzetto, SMT Techniques for TLA⁺ Proof Obligations, Université de Lorraine. Supervised by Kaustuv Chaudhuri and Stephan Merz, since 10/2010.

Juries

Stephan Merz wrote reports on the following PhD theses:

• Pierre-Emmanuel Cornilleau: Certification of Static Analysis in Many-Sorted First-Order Logic, ENS Cachan-Bretagne;

• Mélanie Jacquel: Automatisation des preuves pour la vérification des règles de l'Atelier B, CNAM Paris;

• Chantal Keller: A Matter of Trust: Skeptical Communication Between Coq and External Provers, Ecole Polytechnique;

• Yan Zhang: Semi-Automatic Controller Design in a Java-like Language, Université Paris 6.

He also was a member of the PhD committees of Dorin Maxim and Faqing Yang in Nancy.

Thomas Sturm was a member of the PhD committee of Evgeny Kruglov in Saarbrücken.