Research Topics
I have worked in two distinct areas of research: the first (chronologically) involves theoretical computer science, logic and automata theory, and the second focuses on applications and development in computer music.
The link between both activities is the processing of tree structured data.
Computer Music and Music Notation Processing
Automated Music Transcription
Conversion of a performance into music notation.
We are developing an approach for the transcription of MIDI recordings of performances into digital music scores, based on an abstract intermediate representation of music notation as trees, and on advanced quantitative parsing algorithm. It is implemented into the
qparse library, and experiments have shown very good results on challenging datasets.
Read more
Tree-Structured Representations of Timed Data
An abstract hierarchical intermediate representation of music notation.
This abstract model of digital musical score is used as an intermediate representation in applications related to the processing of written music. Its principle is that, like in symbolic music notation, durations are defined hierarchically, be recursive division of time-spans.
Read more
Comparison of Digital Music Scores
diff-like procedures for XML digital music scores.
We consider the problem of computing the differences between two digital music scores, given in an XML encoding (
MusicXML or
MEI), and visualizing these differences side-to-side.
Read more
Pitch Spelling
Estimation of note names from their pitch in number of semitones.
We revisit the old problem of Pitch Spelling (PS), and local and global tonality guessing, with a new algorithm for their joint estimation. It searches for an optimal spelling based on current conventions for music notation, and musicological tools such as distances between tonalities.
Read more
Symbolic Weighted Automata
Quantitative language models computing over infinite alphabets.
A study of some classes of automata and transducers processing words and trees over infinite (or large) alphabet and returning a weight value in a semiring, and applications to quantitative parsing.
Read more
Test and Verification of Realtime Interactive Music Systems
Automated generation of test sets for functional reliability and temporal predictability.
Supervision of the development of a platform for conformance testing of the real-time Interactive Music System (IMS)
Antescofo, as part of Clément Poncelet’s PhD (2013-2015).
Read more
Formal Tree Languages, Automated Reasoning and Structured Data Processing
Constrained Tree Automata
Classes of Tree Automata that can check syntactic equalities and disequalities of subtrees.
We study automata formalisms computing on trees of finite rank, labeled by symbols from a finite alphabet, extended by constraints, and different applications of these formalisms.
Read more
Term Rewriting Systems
Decision problems in term rewriting, for automatic deduction and verification.
For a Turing-complete computational model such as term rewriting, it is natural to ask about the decidability (in the general case or in specific cases) of certain properties, such as the accessibility of a given term from another by rewriting, strong termination (all rewriting sequences terminate), or confluence (two divergent rewriting sequences can always converge to the same term).
Read more
Automation of Inductive Theorem Proving
Developing an ITP system for the certification of critical systems.
Inductive Theorem Proving (ITP) is used to establish the validity of conjectures in particular structures such as natural numbers, lists, and binary trees (referred to as initial models). This technique is widely used for the certification of critical applications in Computer Science and Artificial Intelligence. Inductive validity is undecidable in general, and the automation of ITP has been investigated by the automated reasoning community for decades,
facing major challenges.
Read more
Hedge Automata and Rewriting, Data Tree
Verification of XML transformations and navigation languages.
We study various automata formalisms for processing ranked trees labeled with data or unranked trees (hedges), and their use in methods such as Regular Model Checking and Type Verification.
Read more
Specification and verification of security protocols
former research topic (1999-2005)
Security protocols describe messages exchanged by agents in a hostile environment and composed using cryptographic primitives. They are sometimes described in scientific literature using a semi-formal notation known as Alice-Bob language, which specifies the content of messages between protocol actors (agents). This syntax can be seen as a textual representation of Message Sequence Charts used in RFCs, among other places. This language is simple and concise for describing the overall flow of a protocol, but it is nevertheless ambiguous and obscures the local operations of each agent.
Read more
