Research scientist at Inria, member of Vertigo team, on leave at the Cedric lab, CNAM, Paris. With a background on formal methods for systems and software verification, my current research project is concerned with the processing of symbolic music data, in collaboration with specialists in Score Databases, Musicology and Computer Aided Composition.
new version of the qparse library for automated music transcription.
My research project is concerned with Computer Music and Digital Humanities, more specifically with the processing of structured music data (digital music scores), and in particular the following problems:
using on formal methods and tools from the following fundamental domains:
Formerly, I have worked on these formal methods and their application to the verification of systems and software:
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 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.
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
There are two main use cases of this framework:
Our test framework contains various independent modules (altogether 18 000 locs), such as:
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 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.
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
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/.
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.
During my post-doc at MPI-I, 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 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.
Langages a priori en transcription musicale.
co-supervised with Philippe Rigaux.
Modélisation, analyses et exécution de systèmes musicaux interactifs.
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.
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.
Mesures de similarité rythmique dans les bases de partitions numériques.
Representation des données musicales rythmiques.
Multimedia scheduling for interactive multimedia systems.
Quantification musicale avec apprentissage sur des exemples.
Grammaires hors-contexte d’arbres de rang non-borné.
Validation of a framework for automated inductive theorem proving.
Conception et réalisation d’un système de démonstration automatique par récurrence.
Validation des règles de configuration d'un firewall.
Automates d’arbres à mémoire d’ordre supérieur.
Décision de la sûreté des protocoles contre les attaques par dictionnaire.
Specification et certification du protocole de telecommunication Kermit a l’aide du demonstrateur automatique par recurrence Spike.
Complexité de problèmes de décision en unification rigide.
Some lectures and other teaching activities:
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.
18 months exploratory project between IReMus, Ircam/STMS and CNAM-CEDRIC.
Grant of one year by the Yamaha Music Foundation, for a collaboration with Nagoya University and Ircam.
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.
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.
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.
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.
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.
Collaboration to a project leaded by Jean Bresson, at Ircam, on computation, time and interactions in computer-aided music composition.
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.
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.
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.
Participation to the Advanced Investigator Webdam (Prime Investigator Serge Abiteboul), on the theme Foundation of Web data management.
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.
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.
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.
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.
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.
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.
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 :
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.
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.
Chairman of the workshop WTS 2010 (Workshop on Formal Methods for Web Data Trust and Security).
Member of the selection board of ENS Cachan, 2006-2008.
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.