Habilitation
Specification and verification of parameterized systems
Jury
- Jean-Luc Baril
- Sandrine Blazy (reviewer)
- Pierre-Cyrille Heam
- Pascale Le Gall (reviewer)
- Stephan Merz
- Pascal Schreck (reviewer)
Abstract
My research is in the domain of formal methods of specification and verification of models and programs. My first work focused on the verification and synthesis of invariants for distributed systems parameterized by the number of processes run in parallel. Then I studied the correction of imperative programs with respect to temporal properties and formal functional specifications. More recently, I have implemented a method to discover new decision procedures, applied deductive verification to enumerative combinatorics, and adapted rewriting strategies to the formalization of multiscale methods. An important part of my work is about the deductive method, which formalizes the correction of a system by a logical formula, which must then be rigorously proved. I present my contributions to the subject of deductive verification of imperative programs annotated by functional specifications.
The manuscript will be available on https://tel.archives-ouvertes.fr/ after the defense.
The Coq code described in the manuscript is available on request by e-mail.
Ph.D.: Combinatorial enumeration of rooted maps on a surface and a bijection
Jury
MM. Robert Cori
Alexandre Zvonkine
Jean-Yves Thibon
Paul Zimmermann
Didier Arquès
Abstract
A map is a connected graph embedded in a surface. Maps are topological objects which can be counted up to homeomorphism by their number of vertices, edges and faces. Maps admit inner symmetries which make them hard to enumerate. The scope of this work is limited to rooted maps, since rooting eliminates all symmetries.
The exact number of rooted maps on a given surface is only known for surfaces with small genus, like the sphere (genus 0) or the projective plane (genus 1), since the enumeration methods complexity strongly increases with the surface genus.
An important part of this work was to convert such a computational method into a common pattern symbolic proof for all the generating series of rooted maps with positive genus.
For any orientable surface, the problem unknown is reduced to a polynomial whose degree is bounded by a simple function of the surface genus. A similar result is obtained for non orientable surfaces.
These results lead to practical methods for exact enumeration. They have been implemented in a software tool. New explicit formulas are given for enumerations up to genus 3.
Independently, a new bijection between a planar hypermaps family and a polygon dissections family, both counted by Schröder numbers, is described.
KEYWORDS: combinatorics, enumeration, rooted map, surface, generating series.
Manuscript: https://tel.archives-ouvertes.fr/tel-00724977