| 2024 | AINA | Effective Parallel Formal Verification of Reconfigurable Discrete-Event Systems Formalizing with Isabelle/HOL. | Sohaib Soualah, Mohamed Khalgui, Allaoua Chaoui |
| 2020 | ICSoft | Formalization and Verification of Reconfigurable Discrete-event System using Model Driven Engineering and Isabelle/HOL. | Sohaib Soualah, Yousra Hafidi, Mohamed Khalgui, Allaoua Chaoui, Laid Kahloul |
| 2020 | ICSoft | Efficient Verification of Reconfigurable Discrete-Event System Using Isabelle/HOL Theorem Prover and Hadoop. | Sohaib Soualah, Yousra Hafidi, Mohamed Khalgui, Allaoua Chaoui, Laid Kahloul |
| 2018 | IRI | A Graph Transformation Approach to Generate Analysable Maude Specifications from UML Interaction Overview Diagrams. | Chafika Djaoui, Elhillali Kerkouche, Allaoua Chaoui, Khaled Khalfaoui |
| 2017 | IRI | On the Verification of UML State Machine Diagrams to Colored Petri Nets Transformation Using Isabelle/HOL. | Said Meghzili, Allaoua Chaoui, Martin Strecker, Elhillali Kerkouche |
| 2017 | IDEAS | Cloud Service Composition Modeling Using Bigraphical Reactive Systems. | Oussama Kamel, Allaoua Chaoui, Mohamed Gharzouli |
| 2016 | ANT | On TGG Ability for Transforming UML 2 Sequence Diagrams with Imbricate Combined Fragments to π-Calculus Specifications. | Nabil Messaoudi, Allaoua Chaoui, Mourad Derardja, Mohamed Bettaz |
| 2015 | AICCSA | An automatic approach to transform BPMN models to Pi-Calculus. | Riad Boussetoua, Hammadi Bennoui, Allaoua Chaoui, Khaled Khalfaoui, Elhillali Kerkouche |
| 2015 | FNC | An Operational Semantics for UML 2 Sequence Diagrams Supported by Model Transformations. | Nabil Messaoudi, Allaoua Chaoui, Mohamed Bettaz |
| 2015 | FNC | A Framework for Modeling and Analysis UML Activity Diagram using Graph Transformation. | Yasmina Rahmoune, Allaoua Chaoui, Elhillali Kerkouche |
| 2015 | IC3K | Usearch: A Meta Search Engine based on a New Result Merging Strategy. | Tarek Alloui, Imane Boussebough, Allaoua Chaoui, Ahmed Zakaria Nouar, Mohamed Chaouki Chettah |
| 2015 | IRI | Capturing and Verifying Dynamic Program Behaviour Using UML Communication Diagrams and Pi-Calculus. | Aissam Belghiat, Allaoua Chaoui, Mokhtar Beldjehem |
| 2015 | ICSoft | A Pi-calculus-based Approach for the Verification of UML2 Sequence Diagrams. | Aissam Belghiat, Allaoua Chaoui |
| 2010 | CAINE | Mapping UML Components diagrams to XML using Graph Transformation. | Rabah Mokhtari, Allaoua Chaoui, Mohamed Redha Bahri |
| 2010 | TASE | Modeling and Analysis of Reconfigurable Systems Using Flexible Petri Nets. | Laid Kahloul, Allaoua Chaoui, Karim Djouani |
| 2009 | ICDCN | A Formal Framework and a Tool for the Specification and Analysis of G-Nets Models Based on Graph Transformation. | Elhillali Kerkouche, Allaoua Chaoui |
| 2009 | ISCC | Transforming UML models to colored petri nets models using graph grammars. | Elhillali Kerkouche, Allaoua Chaoui, Khaled Khalfaoui |
| 2009 | ISPDC | Distributed Causal Model-Based Diagnosis Based on Interacting Behavioral Petri Nets. | Hammadi Bennoui, Allaoua Chaoui, Kamel Barkaoui |
| 2008 | CAINE | A Tool for Design and Verification of Distributed Manufacturing Process Based on Meta-Modelling and Graph Grammars: Application to a Production Line. | Amel Meliouh, Elhillali Kerkouche, Allaoua Chaoui |