PhD Thesis
- Jaime Arias. Formal Semantics and Automatic Verification of Hierarchical Multimedia Scenarios with Interactive Choices. PhD thesis, Université de Bordeaux, France, 2015.
Jaime Arias
CNRS Research Engineer
- LIPN (Hypatia Building) - Office Y119
- contact me by email
- www.jaime-arias.fr
About Me
I am a CNRS research engineer in the SAFER group at LIPN, Université Sorbonne Paris Nord. I lead the laboratory's development team and serve as Chargé de mission « Logiciels » for CNRS Sciences informatiques.
Research Interests
- Formal specification and verification of concurrent systems
- Interactive multimedia systems
Education
-
Ph.D. in Computer Science 2015Advised by Myriam Desainte-Catherine and Camilo Rueda
-
Engineering Degree in Computer Science 2013Advised by Carlos Olarte
-
Engineering Degree in Electronics 2013Advised by Eugenio Tamura
Software
I design, develop, and maintain open-source research software. Below are the tools I am actively maintaining, followed by past contributions.
Actively maintaining
ADT2AMAS
Tool to translate an Attack-Defence tree (ADTree) model into itsAsynchronous Multi-Agent System (AMAS) model.
CosyVerif
Software environment for the formal specification and verification ofdynamic systems.
Imitator
Tool for parametric verification and robustness analysis of real-timesystems with parameters.
Morfetik
Ressource lexicale morphologique extensible et modulaire pour le français
Best Demo Award at EGC 2026
SOGMBT
Symbolic Observation Graph-Based Generator of Test Paths
Solidity2CPN
Tool for the formal verification of smart contracts using Coloured PetriNets.
Past contributions
Projects
I have been the principal investigator of the following projects:
PISTACHE
2024
PISTACHE
2024
Project funded by Université Sorbonne Paris Nord that aims to reduce the
state-space generated by Maude using the Symbolic Observation Graph.
CORRECTNESS
2024
CORRECTNESS
2024
Project funded by MSH
Paris Nord that aims to give ReativeIS formal and
executable semantics in rewriting logic.
MEASURE
2019
MEASURE
2019
Project funded by Université Sorbonne Paris Nord that aims to use formal
models for guiding music improvisation.
vmo-score
2019
vmo-score
2019
Project funded by MSH
Paris Nord that aims to extend the inter-media sequencer ossia-score with musical
improvisation capabilities using the Variable Markov
Oracle.
Publications
A selection of recent work is highlighted below. The complete list is available on DBLP and HAL.
Selected publications
-
Strategic (timed) computation tree logicAutonomous Agents and Multi-Agent Systems (JAAMAS)
-
Optimal Scheduling of Agents in ADTrees: Specialized Algorithm and Declarative ModelsIEEE Transactions on Reliability
-
CosyVerif: The Path to Formalisms CohabitationApplication and Theory of Petri Nets and Concurrency (Petri Nets)
-
Symbolic Observation Graph-Based Generation of Test PathsTests and Proofs (TAP)
-
ADT2AMAS: Managing Agents in Attack-Defence Scenarios.Autonomous Agents and Multi-Agent Systems (AAMAS)
Theses
Engineering Degree Thesis
- Jaime Arias. Model checking for TCC calculus. Engineering's thesis, Universidad Javeriana, Cali, Colombia, 2013. Diploma Thesis
Responsibilities
-
Chargé de Mission (Logiciels) Since 2025CNRS Sciences Informatiques
-
Member (GT3) Since 2024Collège Codes Sources et Logiciels
-
Head of the Software Committee Since 2023LIPN
-
Head of the Development Team Since 2021LIPN
-
Ambassador Since 2021Software Heritage
-
Board Member 2021–2025Galilée Doctoral School
Service
Roles in the organisation and reviewing of international conferences, workshops, and journals.