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.