Experience

Inria Paris and Cedric lab, CNAM, France

Research Scientist • Jan. 2017 — Present

I currently conduct research on Computer Music, and more specifically in processing of structured music data (XML digital music score)

  • creation, digitalisation (assistance to composition and corpus captation),
  • management (information retrieval in bases of music scores) and
  • analysis (digital musicology).

Ircam, Inria Paris, France

Research Scientist in team Mutant (team leader Arshia Cont) • Jan. 2012 — Dec. 2016

Verification of Realtime Interactive Music Systems and Constraint Solving for Symbolic Music Representation.

LSV/ENS Cachan, Inria Saclay, France

Research Scientist in team Dahu, vice responsible of the project (project leader Luc Segoufin) • Jan. 2008 — Dec. 2011

In this team on verification on Databases, my activities focused on typing formalisms and XML schemas, verification and typechecking of tree transformations and XML updates, verification of XML access control policies.

LSV/ENS Cachan, Inria Saclay, France

Research Scientist in team Secsi, vice responsible of the project (project leader Jean Goubault-Larrecq) • May 2002 — Dec. 2007

Secsi stands for security in information systems and in this team I worked in symbolic verification of security protocols.

Trusted Logic SA, Versailles, France

Research Engineer • Jan. 2001 — Apr. 2002

I spent two years mobility in the company TL specialized in in the develpement and certification of secure and open software technology for embedded systems (CEO Dominique Bolignano) where I had activities on conception of tools for static analysis of JavaCard programs, Common Criteria certification of a smartcard OS, development of an interoperable open framework for mobile payment terminals.

LORIA, Inria Nancy, France

Research Scientist in team Protheo (project leader Hélène Kirchner) • Oct. 1998 — Dec. 2000

In this team focused on automated deduction, I had activities in particular in inductive theorem proving and infinite state system verification methods applied to functional programs and security protocols.

Max Planck Institut für Informatik, Saarbrücken, Germany

Post-doctoral researcher in Programming Logic Group (group leader Harald Ganzinger) • Jan. 1997 — Sept. 1998

During this 20 months long post-doctoral stay in the research group of Harald Ganzinger on Automated Deduction, I had activities in first order theorem proving (with some contribution to the theorem prover SPASS), symbolic constraint solving and extended tree automata theory.

SRI International Computer Science Laboratory Menlo Park, CA, USA

Research Fellow in project Maude (project leader Jose Meseguer) • Nov. 1996 — Dec. 1996

Development of a tree automata module for the Maude system.

Education

École Normale Supérieure de Cachan

Habilitation a diriger des recherches, Computer Science • 2011

Extended Tree Automata Models for the Verification of Infinite State Systems. Examination board Jean-Pierre Jouannaud (president, reviewer), Christoph Löding, Denis Lugiez, Luc Segoufin (examiners), Helmut Seidl, Sophie Tison (reviewers).

University Paris XI, Orsay, France

PhD in Computer Science • 1993 — 1996

Tree Automata and Term Rewriting. Supervisor Hubert Comon. Examination board Bruno Courcelle (president), Sophie Tison, Michael Rusinowitch (reviewers), Hubert Comon, Harald Ganzinger, Brigitte Rozoy (examiners).

University Paris XI, Orsay, France

Master Thesis in Computer Science • 1993

École Normale Supérieure de Paris, France

Master in Fundamental and Applied Mathematics and Computer Science of Paris • 1992 — 1993

Research

My research project is concerned with Computer Music and Digital Humanities, more specifically with the processing of structured written music data (digital music scores), in particular the problems of:

  • Automatic Music Transcription
  • Melodic Similarity computation
  • Digital Music Score and Corpora Analysis (Digital Musicology)
  • Information Retrieval in collections of digital music scores

The agenda for tackling these problems is to apply and contribute to research on formal methods and tools issued from the following fundamental domains:

  • Theory of Automata and Tree Automata, weighted and unweighted,
  • Edit Distances between strings and trees,
  • Logic for Computer Science,
  • Term Rewriting Systems.

Formerly, I have worked on these formal methods and their application to the verification of systems and software:

  • Interactive Music Systems, Real-Time Testing and Computer-Aided Composition at Ircam, Paris (team Mutant),
  • Verification of Web data management systems and Computer Security at LSV/ENS-Cachan,
  • Automated Deduction at Inria Nancy, MPI-I Saarbrücken, SRI International, Stanford,
  • development of secure embedded software components for smartcards and payment terminals at the company Trusted Logic.

Publications

Selected publications in reverse chronological order (in our community, the authors are generally listed by alphabetic ordering).

Software

qparse

Inria • 2017 — Present • sources: https://gitlab.inria.fr/qparse/qparselib

qparse is a C++ library for automated music transcription.

It converts a symbolic musical performance, given as a sequence of musical events with arbitrary dates and durations (typically an unquantified MIDI file), into a structured music score. Several output formats are possible, including MEI and Lilypond.

The transcription procedure is based on a prior language model of musical scores describing the prefered music notations. In contrast to other tools using on sequential models (Markov chains), our language model (weighted tree automata) is hierarchical, allowing to take into account the deep structure of common Western rhythm notation (musical meter, rhythms beaming etc). Such languages can be built using several methods, in particular they can be learned from corpora, for a transcription in a given notational style.

Transcription then works by parsing the input against the language model. It chooses a optimal output score according to criteria of fitness to input and conformity to the prior language. Several models of performances are available for evaluating the fitness of score to input events, including stochastic models and models based on tropical algebra. The transcription can be performed offline, on an input file recording a performance, but also online, given an input stream (e.g. from a MIDI keyboard), thanks to the efficient Dynamic Programming algorithms for parsing.

RQ

Ircam • 2016 • sources: https://forge.ircam.fr/p/omlibraries/downloads/

RQ is an environement for rhythm quantization, integrated into the graphical programming environment OpenMusic, a state of the art system in computer assisted music composition developed at and distributed by Ircam.

The quantization procedure of RQ follows an interactive workflow, favouring user interactions in order to search for a satisfying balances between different criteria, in particular the precision of the transcription and the readability of the music score in outcome. It has been implemented via a dedicated graphical interface making it possible the interactive exploration of the space of quatization solutions (rendered in music notation) their visualization and their edition, with a particular focus on the processing of grace-notes and rests.

Most of the developpement of RQ was conducted by Adrien Ycart, at Ircam, in collaboration with Jean Bresson (main developper of OpenMusic) and it has been evaluated by some composers and musicologists.

Antescofo realtime testing enrironment

Inria, Ircam • 2014 — 2017

This work was realized by Clement Poncelet-Sanchez during its phd, in the context of the developpement of the score-based Interactive Music System (IMS) Antescofo by team Mutant at Ircam.

The general objective is to provide techniques and tools to assist both programmers of mixed music scores (i.e. composers) and the developers of the system itself in predicting statically the behavior of the IMS (more specificaly, the problems of functional reliability and temporal predictability) in response to every possible musician input. It should be outlined that the former are generally not experts in real-time programming, and we aim at giving them a clear view of what will be the outcome of the score that they are writing, and what are the limits of what is playable by the system. These verifications cannot be done manually because of the amount of unpredictable human interactions and timing constraints (for audio computations) involved.

We have built a framework for automated timed conformance testing, based on

  • a formal definition of the semantics of the language (DSL) of mixed music scores,
  • advanced symbolic state exploration techniques (model checking).

There are two main use cases of this framework:

  1. Test of Antescofo on a given real score, in a context of the preparation of a concert.
  2. Test on toy scores in order to debug some particular feature of the system.

Our test framework contains various independent modules (altogether 18 000 locs), such as:

  • A frontend compiler of scores in Antescofo DSL into IR models, on the top of Antescofo Flex/Bison parser (13 000 C++ locs);
  • Command-line tools and scripts for convenience conversion and comparison of timed input and output traces including an adapter for online workflow;
  • Convenience Scripts for deployment of the UPPAAL Suite in our workflow;
  • specific adapter function for the Antescofo Standalone version. Documentations are provided to permit an easy use and understanding of the framework.

Antescofo

Inria, Ircam • 2012 — 2017

Antescofo (main developper Arshia Cont) is a polyphonic Score Following system for mixed music live performance (involving computers and analog instruments). This system allows for real-time automatic recognition of the position in a music score and the tempo, from an audio stream coming from performer(s) (artificial listening module), and for synchronization of pre-written computer realized elements to this instrumental performance (player module). Both the computer-played elements and the instrumental score, as well as instruction for their synchronization, must be written in a Domain Specific Language (DSL) and given in input to the system.

In the context of Inria’s team Mutant at Ircam, I collaborated to the developpement of this Interactive Music System, with contributions in particular to Antescofo’s parser and standalone system, and supervision of the development of timed-testing procedures.

Antescofo has been initially released as a patch for the real-time music environement Max, and distributed via Ircam’s Forum. A standalone version and an
editor for the DSL of input music scores have been developped later in team Mutant. This software was finaly transfered to the eponymous startup Antescofo at its creation in 2016.

TACE

Inria, LSV/ENS Cachan • 2006 • sources: http://tace.gforge.inria.fr

TACE is an OCaml library implementing procedures for the construction and decision of several classes of Tree Automata with Constraints of Equality modulo Equational Theories.

It designed as a specialized first order theorem prover, following the approach presented in Tree automata with equality constraints modulo equational theories, JLAP 75(2) 2008 - coauthored with Michaël Rusinowitch, and Laurent Vigneron.

The library TACE has been applied to the verification of security protocols in models with explicit destructors. It was also used as an algorithmic toolbox for the integration of decision procedures in inductive theorem proving procedures and later for the problems of XML static typechecking the verification of XML access control policies.

Java Card

Trusted Logic • 2000 — 2002

I have worked at the company Trusted Logic, on the development and certification of software components for embedded systems, in particular smartcards and payment terminals.

More specificaly, I worked there on the conception of tools for the formal verification of Java and JavaCard programs, based on symbolic evaluation methods.

I was also involved in the development of an open multi-platform environment for payment and mobile terminals, with in particular the realization of

  • components of a HAL (Hardware Abstraction Layer) enabling the port of the environment (to STIP profile terminals, FINREAD card readers and MIDP mobile terminals),
  • some applications for terminals,
  • a terminal simulator for running and debugging applets on a PC environment (Win32).

CASRUL

Inria Nancy, LORIA • 1999 — 2000

I developped at Inria Nancy the first version of the system CASRUL, a security protocol verification tool based on deduction rules.

This implements a procedure for compiling semi-formal protocol specifications into multiset rewrite rules describing precisely the operations of the agents for the analysis of the received messages and the construction of the sent messages, as well as the faculties of the attackers. The translation of this intermediate language into input format (Horn clauses) for the daTac theorem prover (developped by Laurent Vigneron), allows a formal verification of the protocols using first-order deduction procedures such as narrowing.

The approach is presented in Compiling and verifying security protocols, 7th international conference on Logic for programming and automated reasoning LPAR’00, Springer LNAI 1955, co authored with Michaël Rusinowitch and Laurent Vigneron – see also https://hal.inria.fr/inria-00072712/.

This system CASRUL has later evolved into a tool-suite developed during the European projects AVISPA and AVANTSSAR.

SPASS

MPI-I • 1997 — 1998

SPASS (main developer Christoph Weidenbach) is a first order theorem prover based on the superposition calculus, developped at the Max-Planck Institut für Informatik, Saarbrücken, Germany.

I have made minor contributions to the development of this automated deduction system, implementating in particular approximation methods and Horn clauses transformation functions for the purpose of unification modulo sorted equational theories. This work was done in callaboration with Christoph Weidenbach and Christoph Meyer.

Maude

SRI International • 1996

Maude is a declarative language based on Rewriting Logic, developped by Steven Eker, under the direction of Jose Meseguer, at S.R.I. International, Computer Science Laboratory, Palo Alto, CA, USA.

I implemented (C++) tree automata tools in the virtual machine of the language, the the development of an inductive theorem prover in Maude thereafter.

Students

PhD Students

Lydia Rodriguez de la Nava (INRIA, EDITE Paris) • 2020 — 2023

Structured Models for Written Music Processing.
co-supervised with Philippe Rigaux.

Francesco Foscarin (CNAM, EDITE Paris) • 2017 — 2020

Langages a priori en transcription musicale.
co-supervised with Philippe Rigaux.

Francesco is now a post-doc at JKU in Vienna. Previously (2021), it has held a temporary lecturer and research assistant position at CNAM.

Pierre Donat-Bouillud (Ircam, EDITE Paris) • 2016 — 2019

Modélisation, analyses et exécution de systèmes musicaux interactifs.

Pierre is now post-doc at the Northeastern, Programming Research Lab in Praha, in the ERC project Evolving Language Ecosystems (ELE).

Clément Poncelet-Sanchez (Ircam, EDITE Paris) • 2013 — 2016

Méthodes formelles d’analyse d’interactions homme-système dans des scénarios temporels complexes.

Clement is currently in post-doc in the Computational Systems group at the Software Systems Center of Salzburg University.

Stéphanie Delaune (ENS Cachan) • 2003 — 2006

Verification of cryptographic protocols with algebraic properties.
co-supervised with Hubert Comon-Lundh, Francis Klay.

Stéphanie is now CNRS senior research scientist at Irisa, Rennes.

Master and Engineer Students

Clément Buon (Master 1st year INALCO, Université Sorbonne Paris Cité) • 2023

development of a MusicXML export facility from an Intermediate Representation of digital music scores.

Augustin Bouquillard (Licence (Bachelor last year) University Paris Dauphine, PSL) • 2023

Pitch Spelling algorithms for Jazz.

Teysir Bouaeb (Master 1st year ENSTA, Intitut Polytechnique de Paris) • 2022

Parameter optimisation for an Automatic Music Transcription procedure on a monophonic dataset.

Augustin Bouquillard (Licence (Bachelor 3d year) University Paris Dauphine, PSL) • 2022

Study of an voice separation algorithm in the context of piano transcription.

Martin Digard (Master, 2d year INALCO, Université Sorbonne Paris Cité) • 2021

Automated Drum Transcription.

Leyla Villaroel (Master Pontificia Universidad Católica de Chile, internship at CNAM) • 2021

On-the-fly music transcription (funded by a program between Inria Chile and Chile Universities).

Henry Boisgibault (M1 SupElec, internship at CNAM) • 2017

Mesures de similarité rythmique dans les bases de partitions numériques.

Florent Mercier (Master U. Paris 11, internship at Ircam) • 2017

Representation des données musicales rythmiques.

Pierre Donat-Bouillud (Master ENS Rennes, internship at Ircam) • 2016

Multimedia scheduling for interactive multimedia systems.

Adrien Ycart (Master SupTelecom, intership at Ircam) • 2015

Interactive Rhythm Quantisation.

Clément Poncelet Sanchez (Master UPMC, internship at Ircam) • 2014

Environnement de test pour un système temps-réel de performance en musique mixte.

Adrien Maire (L3 ENS Cachan, internship at Ircam) • 2013

Quantification musicale avec apprentissage sur des exemples.

Pierre Donat-Bouillud (L3 ENS Rennes, internship at Ircam) • 2013

Transcription rythmique dans OpenMusic.

Léa Fanchon (Master École Centrale, intership at Ircam) • 2012

Analyse statique des paramètre performatifs dans les partitions de musique mixte.

Guillaume Baudard (Master ENS Rennes, intership at Ircam) • 2012

Antescofo - vers une programmation synchrone.

Adrien Boiret (Master ENS Cachan) • 2010

Grammaires hors-contexte d’arbres de rang non-borné.

Jérémy Dimino (Master ENS Cachan) • 2010

Automates d’arbres et données.

Ryma Abassi (Master Sup’Com Tunis, internship at LSV, ENS Cachan) • 2010

Vérification de politiques de sécurité XACML.

Yoshiharu Kojima (Master Nagoya University) • 2009

Controlled Term Rewriting.

Sawsen Ben Nasr (Master ENSI Tunis, internship at LSV, ENS Cachan) • 2009

Validation of a framework for automated inductive theorem proving.

Hedi Benzina (Master Sup’Com Tunis, internship at LSV, ENS Cachan) • 2008

Conception et réalisation d’un système de démonstration automatique par récurrence.

Mohamed Anis Benelbahri (Master Sup’Com Tunis, internship at LSV, ENS Cachan) • 2008

Validation des règles de configuration d'un firewall.

Camille Vacher (Master ENS Cachan) • 2007

Automates d’arbres à mémoire d’ordre supérieur.

Nicolas Perrin (L3 ENS Lyon, internship at LSV, ENS Cachan) • 2006

Visibly Tree Automata.

Stéphanie Delaune (Master ENS Cachan) • 2003

Décision de la sûreté des protocoles contre les attaques par dictionnaire.

Sanar Sfar (Master Sup'Com Tunis, internship at LORIA, Nancy) • 1999

Specification et certification du protocole de telecommunication Kermit a l’aide du demonstrateur automatique par recurrence Spike.

Véronique Cortier (L3 ENS Cachan, internship at MPI-I Saarbrücken) • 1998

Complexité de problèmes de décision en unification rigide.

Teaching

Some lectures and other teaching activities:

  • lecture on Object Oriented Programming with C++, 2 semesters in 2022-2023 (40 hours / semester)
    at the Master on NLP, 1 year, INALCO, Université Sorbonne Paris Cité

  • lectures at ISR (International Summer School on Rewriting) in July 2019, on Rewriting Music. Slides:
    • intro on Computer Music,
    • part 1 weighted SRS and melodic distance computation,
    • part 2 weighted TRS, music notation processing and automated music transcription.
  • Lecture (3h) for the opening semester seminar 2017 at École Normale Supérieure Paris-Saclay, on Music and Automata.

  • Lecture (6h) at the summer school VTSA 2011 (Verification Technology, Systems & Applications), Liège, Belgium, on Tree Automata Techniques for Infinite Systems Verification.

  • Lecture on Tree Automata Theory at Master Parisien de Recherche en Informatique (MPRI) between 2006 and 2011 (36h/year).

  • Teaching assistant for the lecture of Jean Goubault Larrecq on Lambda Calculus at Master Parisien de Recherche en Informatique (MPRI), École Normale Supérieure de Paris, between 2003 and 2006.

  • Co-author of the collective online book Tree Automata Techniques and Applications, widely used for teaching this discipline in universities.

Projects

Polifonia (H2020-SC6-TRANSFORMATIONS)

A digital harmoniser for musical heritage knowledge

10-2021 — 10-2025

The objective of this European project is to realise an ecosystem of computational methods and tools supporting discovery, extraction, encoding, interlinking, classification, exploration of, and access to, European musical heritage knowledge on the Web, and to demonstrate that these tools improve the state of the art of Social Science and Humanities methodologies.

The partners are Alma Mater Studiorum, Università di Bologna (coordinateur), Open University, Stichting Vrije Universiteit Amsterdam, Insight Centre for Data Analytics, NUI Galway, Istituto Centrale del Catalogo e della Documentazione, Istituto Centrale per i Beni Sonori e Audiovisivi, IReMus/CNRS/SU, Cedric/CNAM, Netherlands Institute for Sound and Vision, Royal Netherlands Academy of Arts and Sciences, Digital Paths srl.

Kakenhi (JSPS foundation)

Automatic transcription based on formal language theory

2020 — 2025

The team Vertigo at Cedric/CNAM and Action Codex collaborate in this Japanese National project on music transcription, with Principal Investigator: Masahiko Sakai (Nagoya University), and Co-investigator: Satoshi Tojo (JAIST).

CollabScore (ANR)

Collaborative spaces for digitalized music scores

10-2020 — 10-2023

This project aims at developing approaches for music score digitalisation in semi-structured formats, with Optical Music Recognition (OMR) and methods for large scale collaborative correction and the valorisation of music collections.

It implies Cedric/CNAM (coordinator), Irisa, IReMus/CNRS/SU, the BnF (French National Library), 2 libraries of Fondation Royaumont, and the company Antescofo.

Codex (Inria Exploratory Action)

Generation and processing digital music scores

10-2020 — 10-2023

role: responsible of the project

Inria Exploratory Action on the formal representation and processing of symbolic musical data and applications to information retrieval in digital music score databases, computational musicology, music transcription and corpus digitization.

This Inria project is hosted by the Vertigo team at CNAM/Cedric and is carried out in collaboration with musicologists at IReMus, Ircam/STMS and librarians at BnF.

PolyMIR (emergence Sorbonne Universités)

Music Information Retrieval in Polyphonic Corpora

2017 — 2018

18 months exploratory project between IReMus, Ircam/STMS and CNAM-CEDRIC.

Jido Sayfu 採譜 (Yamaha Music Foundation)

Rhythm Transcription

04-2017 — 04-2018

role: co-PI with prof. Masahiko Sakai (Nagoya University).

Grant of one year by the Yamaha Music Foundation, for a collaboration with Nagoya University and Ircam.

Munir (ANR-FRQSC-2)

Music Notation Information Retrieval

2017 — 2020

Project between CEDRIC/CNAM and Mc Gill and Montréal U.
I co-direct, with Philippe Rigaux at CNAM, the PhD of Francesco Foscarin on transcription, funded by this project.

RQ (Ircam Unité-Projet Innovation)

2016

role: Principal Investigator

Project internaly funded by Ircam for the development of an OpenMusic Library for Rhythm Quantification.

The project was co-coordinated with Jean Bresson, main developper of OpenMusic, most of the developpement was done by Adrien Ycart hired as development engineer … in collaboration with composers and musicologists.

GioQoso (CNRS defi Mastodons 2016)

2016 — 2018

Project between French National Library BnF Paris, Vertigo team in Cedric CNAM, CESR Tours, IReMus Paris, team DKM/Shaman at Irisa, Lannion on methods and tools for the quality management of data in collaborative corpora of digital music scores.

MusICAL (RNSC)

2015

Thematic network of the RNSC (National Network on Complex Systems) on interactive algorithmic composition and languages applied to music, involving Ircam (UMR 9912 STMS), AlgoMus from Universities Lille 1 and Picardie Jules Verne, LaBRI form University Bordeaux, Grame (Centre National de Création Musicale, Lyon), IReMus from Universities Paris-Sorbonne / CNRS / BnF and UMI UMMISCO IRD / UPMC.

LETITBE (PHC Amadeus)

Logical Execution Time for Interactive and Composition Assistance Music Systems

2015 — 2016

role: responsible for the french side

2 years partnership (Partenariat Hubert Curien Amadeus, France-Austria) between the Computational Systems group at the Software Systems Center of Salzburg University and Inria’s team Mutant at Ircam, Paris, on Logical Execution Time For Interactive Music Systems. The main objective of the project was the application to the development of interactive music systems of programming paradigms and formal techniques and tools for real-time critical embedded software. The PhD of Pierre Donat-Bouillud has started during this project.

EFFICACe (ANR JCJC SIMI 2)

2013 — 2015

Collaboration to a project leaded by Jean Bresson, at Ircam, on computation, time and interactions in computer-aided music composition.

Inedit (ANR ConInt)

2012 — 2015

Project between Ircam (UMR 9912 STMS), LaBRI (University Bordeaux) and Grame (Centre National de Création Musicale, Lyon) on authoring of time and interaction in real-time computer music.

Brick (Inria-DGRSRT)

2010 — 2011

role: coordinator for the french partner

Bilateral project (Inria-DGRSRT program STIC Tunisie) between the teams Cassis (Nancy, Inria), Dahu (Saclay, Inria) and Digital Security Group (Tunis, Sup’Com) on the theme Formal verification of Web Services Security, XML Access Control Policies and Firewalls.

ACCESS (ARC Inria)

2010 — 2011

role: coordinator

Action de Recherche Collaborative involving the Inria teams Cassis and Pareo (Nancy), Mostrare (Lille) and Dahu (Saclay), on the theme Access Control Policies for XML, Verification, Enforcement and Collaborative Edition.

Webdam (ERC)

2009 — 2013

Participation to the Advanced Investigator Webdam (Prime Investigator Serge Abiteboul), on the theme Foundation of Web data management.

FireB (Inria-DGRSRT)

2008 — 2009

role: coordinator

Bilateral project (Inria-DGRSRT program STIC Tunisie 2008) between the teams Cassis (Nancy, Inria), Dahu (Saclay, Inria) and Digital Security Group (Tunis, Sup’Com) on the theme automated verification of firewall conformance to access control policies.

FoX (STREP FP7 ICT - FET-open)

Music Notation Information Retrieval

2008 — 2010

Research network involving Inria team Dahu (LSV, ENS Cachan), University of Oxford, Dortmund T. University, The University of Edinburgh, Universiteit van Amsterdam, Hasselt University, Uniwersytet Warszawski on Safe Processing of Dynamic Data over the Internet.

AVOTÉ (ANR Sesur)

2007 — 2009

Project between France Télécom R&D, Inria team SECSI at LSV (ENS Cachan), team Cassis at LORIA (Inria Nancy) and team DCS at Verimag (Grenoble) on the Formal Analysis of Electronic Voting Protocols.

SyDRA (Inria-DGRSRT)

2006 — 2007

role: coordinator

Bilateral project (Inria-DGRSRT program STIC Tunisie 2006) between the Inria team Secsi (Saclay), the LaBRI (U. Bordeaux) and the team Digital Security (Tunis, Sup’Com) on the theme Automated inductive theorem proving techniques for the validation of protocols and distributed systems.

Rossignol (ACI Securite Informatique)

2003 — 2006

role: responsible for the partner LSV/ENS Cachan

Action Concertee Incitative between team MOVE (LIF, Marseille), team SECSI (Inria, LSV/ENS Cachan) and VERIMAG (Grenoble) on Algebraic properties and probabilistic models of security protocols.

Prouvé (RNTL)

2003 — 2006

Project between CRIL Technologies, France Telecom R&D, LORIA Inria Lorraine, Inria team SECSI at LSV ENS Cachan, Verimag (Grenoble) on Automated Verification Tools for Cryptographic Protocols.

EVA (RNTL)

2000 — 2001 (at Trusted Logic) and 2002 — 2003 (at LSV)

role: responsible for the industrial partner Trusted Logic, responsible for the academic partner LSV/ENS Cachan

Project between LSV (ENS Cachan), VERIMAG (Grenoble) and Trusted Logic SA (Versailles) on the theme Explanation and verification of cryptographic protocols. The goal of this project is the highly automatized formal verification of cryptographic protocols and the production of proof explanations, i.e. attacks scenario or certification documents (e.g. in the framework of Common Criteria).

The main realizations of the project are :

  • the development of prototypes of tools for the automatic verification of protocols based on model checking procedures and methods for the automatic computation of relevant finite abstractions of infinite models ;
  • the conception of a base of protocols, as case studies, in a syntax defined for the purpose of the project ;
  • the development of proof explanation tools.

AVISS (IST FP6 FET-open)

2000 — 2001

role: contribution to the preparation and submission

1 year assessment project between Universitat Freiburg, University Genova, Inria team Protheo at LORIA, Nancy on Automated Verification of Infinite State Systems. It has been followed by the IST FET-open project AVISPA involving the same partners.

CALIFE (RNRT)

1999 — 2000

Participation to the RNRT (National Network for the Research on Telecommunications) project CALIFE between INRIA Lorraine, Labri (Bordeaux), LSV/ENS Cachan), France Télécom R&D, DCRIL Technology and Alcatel, on the theme Environment for Formal Proof and Test of Algorithms used in Telecommunication.

Community

  • Member of the Program Committee of the conferences:
    • Journées d’Informatique Musicale (JIM 2016)
    • 2d International Conference on Technologies for Music Notation and Representation (TENOR 2016)
    • 8th International Symposium on Symbolic Computation in Software Science (SCSS 2017)
    • IJCAR 2012 (6th International Joint Conference on Automated Reasoning)
    • TTATT 2012 (1st International Workshop on Trends in Tree Automata and Tree Transducers)
    • RTA 2011 (22nd International Conference on Rewriting Techniques and Applications)
    • CRISIS 2008 (3d International Conference on Risks and Security of Internet and Systems)
    • FOSSACS 2007 (10th International Conference on. Foundations of Software Science And Computation Structures) in ETAPS European Joint Conferences on Theory and Practice of Software)
    • RTA 2005 (16th International Conference on Rewriting Techniques and Applications)
  • Chairman of the workshop WTS 2010 (Workshop on Formal Methods for Web Data Trust and Security).

  • Member of the selection board of Inria junior research scientists at Inria Lille, 2013.
  • Member of the selection board of Université de Paris-Est Créteil, 2012.
  • Member of the selection board of Université de Lille I, 2011.
  • Member of two selection boards for Inria Research Engineer (IE) recruitments in 2009.
  • Member of the selection board for Inria Research Engineer recruitment in 2008.
  • Member of the selection board of ENS Cachan, 2006-2008.

  • Phd examination boards:
    • Nicolas Guiomard Kagan (reviewer), 2017;
    • Emil Andriescu (examiner), 2016;
    • Etienne Dubourg (reviewer), 2016;
    • Carles Creus (examiner), 2016;
    • Vincent Hugo (examiner), 2013.
    • Hedi Benzina (examiner), 2012;
  • Member of the IFIP WG 1.6 on Rewriting; 2014-2017.
  • General Secretary of ASTI, federation of associations in Computer Science; 2003-2011.
  • Treasurer and member of the board of AFIT, the French Association for Theoretical Computer Science, french chapter of the European Association for Theoretical Computer Science; 1998-2002.

  • Coordinator of an action Cooperation of methods for Software Verification, theme : quality and safety of software and systems, Contrat de Plan État Région Lorraine, LORIA, Inria Nancy, 2000.