I am actively participating in the development of the following tools:

  • Imitator: Tool for parametric verification and robustness analysis of real-time systems with parameters.
  • CosyVerif: Software environment for the formal specification and verification of dynamic systems.
  • ADT2AMAS: Tool to translate an Attack-Defence tree (ADTree) model into its Asynchronous Multi-Agent System (AMAS) model.
  • PMC-SOG: Parallel and distributed model checking using the Symbolic Observation Graph (SOG).
  • VMO-Score: Tool to create an i-score interactive score to control the improvisation generated from VMO according to larger structures found in an audio recording.
  • SyMoN: Symbolic model checker for the non-deterministic timed concurrent constraint calculus NTCC.

Over the last years, I have contributed to the following tools:

  • PyHRF: Tools to analyze fMRI data focused on the characterization of the hemodynamics.
  • ReactiveSessions: Library for the specification of communication-based software featuring declarative, reactive, timed and contextual behaviors.
  • T-Calculus: Reactive/real-time programming language prototype embedded in Haskell.
  • I-score: A free and open-source inter-media sequencer.
  • ReactiveIS: Synchronous programming language for writing and executing interactive scenarios.
  • RItMos: Interpreter of interactive multimedia scenarios implemented in the reactive synchronous language ReactiveML, and endowed with a graphical feedback of the execution in INScore.
  • tccMChecker: Model checker for the timed concurrent constraint calculus TCC.