Florent Jacquemard

2 rue Simone Iff 75589 Paris Cedex 12 France · +33 1 80 49 43 23‬ · +33 6 50 08 84 53 · first.lastname@inria.fr

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.

News

Research

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:

  • music transcription
  • music score and corpus analysis (digital musicology) and melodic similarity computation
  • information retrieval in bases of music scores

using on formal methods and tools from the following fundamental domains:

  • automata and tree automata theory, weighted and unweighted,
  • edit distances between strings and trees,
  • logic in computer science,
  • term rewriting systems and automated deduction.

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

  • timed-testing of interactive music systems and Computer-Aided Composition at Ircam, Paris (team Repmus),
  • 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

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

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.

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

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

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

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

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

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

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

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:

  • 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

PolyMIR (emergence Sorbonne Universités)

Music Information Retrieval in Polyphonic Corpora

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

2017 — 2018

Jido Sayfu 採譜 (Yamaha Music Foundation)

Rhythm Transcription
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.

04-2017 — 04-2018

Munir (ANR-FRQSC-2)

Music Notation Information Retrieval

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.

2017 — 2020

RQ (Ircam Unité-Projet Innovation)

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.

2016

GioQoso (CNRS defi Mastodons 2016)

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.

2016 — 2018

MusICAL (RNSC)

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.

2015

LETITBE (PHC Amadeus)

Logical Execution Time for Interactive and Composition Assistance Music Systems
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.

2015 — 2016

EFFICACe (ANR JCJC SIMI 2)

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

2013 — 2015

Inedit (ANR ConInt)

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.

2012 — 2015

Brick (Inria-DGRSRT)

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.

2010 — 2011

ACCESS (ARC Inria)

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.

2010 — 2011

Webdam (ERC)

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

2009 — 2013

FireB (Inria-DGRSRT)

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.

2008 — 2009

FoX (STREP FP7 ICT - FET-open)

Music Notation Information Retrieval

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.

2008 — 2010

AVOTÉ (ANR Sesur)

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.

2007 — 2009

SyDRA (Inria-DGRSRT)

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.

2006 — 2007

Rossignol (ACI Securite Informatique)

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.

2003 — 2006

Prouvé (RNTL)

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.

2003 — 2006

EVA (RNTL)

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.

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

AVISS (IST FP6 FET-open)

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.

2000 — 2001

CALIFE (RNRT)

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.

1999 — 2000

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.