Projects

I led the following projects:

  • MEASURE: Project funded by Paris University 13 that aims to use formal models for guiding music improvisation.

Currently, I participate in the following projects:

  • AESIR: PHC AURORA project funded by Campus France that aims to develop symbolic reachability methods for broad classes of real-time (rewrite) systems; sound and complete untimed and timed temporal logic model checking procedures; and a novel timed strategy language, allowing to analyze a system whose executions are controlled by a user-defined strategy.
  • MoSART: Project funded by CNRS that aims to develop a framework to model and verify multi-agent systems under time constraints. The proposed approach will encompass both theory (definition of formalisms, and decidability) and practice (tool implementation).

Over the last few years, I have participated in the following projects

  • ESPRiTS: Project funded by CNRS that aims to bridge Parametric Timed Automata (PTA) and Real-Time Maude (RTM) so that parametric analyses can be applied to RTM models, thus extending the applicability of these methods. Such techniques will be applied to the analysis of attack-defense trees.
  • SEMANTIQUE: Project funded by Paris University 13 that aims to give ReactiveIS a formal semantics that captures both temporal and spatial constraints in interactive scores. To this end, we will propose an executable Rewriting Logic semantics that will make ReactiveIS more robust and expressive.
  • CoGITARe: Project funded by ANR that aims to develop a mathematical framework for the analysis of quantitative properties of programs by combining two emerging types systems: graded types and intersection type systems; with well established techniques from the field of abstract interpretation such as widening.
  • IFD: Project funded by the Institut Français that aims to develop new parameter synthesis algorithms to find the timing parameters for which a real-time system is safe, and its energy consumption is minimal.
  • PARTIES: Project funded by CNRS that aims to develop a new framework to model and verify multi-agent systems relying on timed strategic logics with incomplete information to multi-player cooperation, with possibly parametric timing information.
  • PAMPAS: PHC Van Gogh project funded by Campus France that aims to develop new algorithms for parallel model-checking and parameter synthesis.
  • AMoJAS: Project funded by Paris University 13 that aims to use the verification techniques for Tight Durational Concurrent Games Structures (TDCGS) for the analysis of Attack-Defense Trees.
  • MUSICAL: Project funded by CNPq that aims to develop and integrate tools from logic and concurrency theory for the design and analysis of reactive systems and their application to musical processes and multimedia systems.
  • PoSET: Project funded by INRIA that aims to provide a consistent and robust mathematical framework for the modeling of sequential and parallel aspects of temporal media in order to develop simpler, safer and more powerful tools for the creation of hierarchical, multi-scale and multi-modal pieces of interactive art.
  • OSSIA: Project funded by ANR that aimed to formalize the logical and temporal constraints inherent in multimedia scenarios in order to develop tools for their specification and verification.
  • REACT+: Project funded by COLCIENCIAS that aimed to develop the underlying theory and machine-assisted tools for verifying concurrent systems specified in the non-deterministic timed concurrent constraint calculus called NTCC, and their application in emergent domains such as Security , Biology and Multimedia Interaction.