Nicolas Halbwachs - Curriculum vitae#

Full CV including a list of publications

Current position: Directeur de Recherche at CNRS, Director of Verimag Laboratory

Education and diplomas

• June 1984 : “State Thesis” in Mathematics, Grenoble
• March 1979 : “Third Cycle Thesis” in Computer Science, Grenoble

Positions occupied

• Since 1992 : Research director at CNRS
• 1992-93 : Invited Professor at Stanford University
• 1980-92 : “Chargé de Recherche” at CNRS

Research Activity

Nicolas Halbwachs' main research results are the following:

• With Patrick Cousot, he designed the “Linear Relation Analysis”, an abstract interpretation for discovering invariant linear inequalities among variables of a program. He adapted the method to the analysis of synchronous programs, and of timed and hybrid systems. I improved it with dynamic partitionning, Cartesian factoring of polyhedra, and abstract acceleration.
• He is one of the founders of Synchronous Programming. With Paul Caspi, he defined the synchronous data-flow language Lustre, devoted to programming embedded software. He sucessively worked on the formal definition of the language, its compilation, its use as a logic for specifying properties (the notion of synchronous observer), the verification of synchronous programs by model-checking and abstract interpretation, the automatic testing of synchronous programs, the use of synchronous programming for modeling non synchronous systems. Lustre is an industrial success-story, as it became the core language of the worldwide used toolset Scade, developed by the company Esterel-technology. Lustre can be considered as a notable success of formal methods in industry.
• Nicolas Halbwachs proposed a method, sometimes called “symbolic bisimulation”, to generate a minimal state graph from an implicit representation (e.g., a Boolean program), the minimality being considered with respect to the bisimulation according to some observation criterion.
• Nicolas Halbwachs designed an automatic method, derived from abstract interpretation, to discover invariant properties about parameterized networks of finite-state processes.
• His most recent work concerns the automatic discovery of invariants in programs manipulating arrays. For instance, our analysis can discover automatically that the result of an “insertion sort” procedure is a sorted permutation of the initial array.

Nicolas Halbwachs published one book, 15 articles in international journals, 46 papers in international conferences, including 11 invited papers. According to Google Scholar, his H-number is currently 31.

Nicolas Halbwachs supervised 10 PhD theses, and about 13 Master theses. He is editor of the journal “Formal Method in System Design”. He co-chaired the Program Committees of conferences CAV’99, TACAS’05 and EMSOFT’09. He took part in more than 30 program committees of international conferences, he was the coordinator of Esprit project LTR 22703 SYRF, and scientific coordinator of a cluster in the FP6 integrated project ASSERT.