Research scientist at Inria, member of Vertigo team, on leave at the Cedric lab, CNAM, Paris. With a background on formal language theory and 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 Digital Music Score Databases and Computational Musicology.
PhD proposal:
Grammar Generative Models for Music Notation Processing.
The objective of this thesis proposal is the development, in the context of musical notation processing, of deep generative models guided by a grammar, in order to produce well-formed structured results.
The main aimed application is the automatic transcription of piano performances recorded in the symbolic MIDI format.
French proposal: Modèles génératifs grammaticaux pour le traitement de la notation musicale
PhD proposal:
Digital Music Score Distances.
This thesis project focuses on the study of similarity metrics and algorithms identifying the differences between digital musical scores, represented in the form of labeled trees.
The targeted applications are the approximate querying of collections of digital music scores, the development of tools for collaborative musical writing and version management and computational musicology, in particular corpus musicology, in collaboration with specialists in this field.
French proposal: Distances entre partitions musicales numériques
poster presentation by Lydia Rodriguez-de la Nava at the 9th International Conference on Digital Libraries for Musicology DLfM 2022, joined with the annual conference of the International Association of Music Libraries (IAML): MIDI To Score Automated Drum Transcription.
paper at WoRMS’22 on Automated Transcription of Electronic Drumkits. slides of the presentation.
talk at Inria’s 1/2h de science, 6 oct. 2022. A 30 min presentation of the Exploratory Action Codex on Musical Notation Processing, at Inria Paris center, with a focus on our activity on transcription.
meeting of the JSPS Kakenhi, 15-16 sept. 2022, Inria center, and Maison Suger, Paris.
paper on the computation of Montgeau-Sankoff edit-distance measuring melodic similarity, based on weighted automata techniques. Information & Computation vol. 282, 2022.
Seminar at EPFL, Bernoulli Centre, organized by the Chair of Discrete Optimization, and in presence of members of the Chair of Discrete Optimization and DCML. title: Automated Music Transcription based on Formal Language Models.
INRIA Exploratory Action Codex (2020-2023) on the formal representation and processing of symbolic music data, and applications to information retrieval in digital music score databases, computational musicology, music transcription and corpus digitization. The project is starting in November 2020 with the PhD of Lydia Rodriguez de la Nava.
Japan national project Kakenhi on Automatic music transcription based on formal language theory (JSPS Foundation, 2020-2025), involving Sakai Lab at Nagoya University and Tojo Lab at JAIST, Kanazawa. We are a funded external partner of the project.
French national project CollabScore (ANR 2020-2023), aiming at the development of approaches for music score digitilization in semi-structured formats, with Optical Music Recognition (OMR) and methods for large scale collaborative correction and the valorization 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.
My research project is concerned with Computer Music and Digital Humanities, more specifically with the processing of structured written music data (digital music scores), and in particular the following problems:
using 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:
list of selected publications since 2007 from HAL (as provided by HAL-INRIA). In reverse chronological order (in our community, the authors are generally listed by alphabetic ordering).
online book Tree Automata Techniques and Applications (pdf).
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/.
This system CASRUL has later evolved into a tool-suite developed during the European projects AVISPA and AVANTSSAR.
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.
Structured Models for Written Music Processing.
co-supervised with Philippe Rigaux.
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.
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).
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.
Tree Automata with Global Constraints for the verification of security properties.
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.
development of a MusicXML export facility from an Intermediate Representation of digital music scores.
Pitch Spelling algorithms for Jazz.
Parameter optimisation for an Automatic Music Transcription procedure on a monophonic dataset.
Study of an voice separation algorithm in the context of piano transcription.
Automated Drum Transcription.
On-the-fly music transcription (funded by a program between Inria Chile and Chile Universities).
Mesures de similarité rythmique dans les bases de partitions numériques.
Representation des données musicales rythmiques.
Multimedia scheduling for interactive multimedia systems.
Environnement de test pour un système temps-réel de performance en musique mixte.
Quantification musicale avec apprentissage sur des exemples.
Analyse statique des paramètre performatifs dans les partitions de musique mixte.
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 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é
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.
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.
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).
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.
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.
18 months exploratory project in digital musicalogy between IReMus, STMS/Ircam and Cedric/CNAM.
Grant of one year by the Yamaha Music Foundation, for a collaboration with Sakai Lab at Nagoya University and Ircam/STMS.
Project between Cedric/CNAM and DDMAL/CIRMMT and Mc Gill University
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 Quantization.
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. It was conducted 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 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 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 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 study of Automated inductive theorem proving techniques for the formal 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 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 projects AVISPA and AVANTSSAR, 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.