3 PhD students (Supervision / Co-supervision)

• KHEIREDDINE Anissa : Parallélisation et optimisation du Bounded model-checking
• SAOULI Sabrine : Exploitation des symétries locales pour les résolutions des problèmes SAT
• XU Hao : Hybridation de méthode de compilation de contraintes, Solveurs SAT, méthodes d'apprentissage pour maîtriser la complexité de la gamme Renault

6 PhD graduated 2013 - 2023

2004-2022 Publications

• 2022
  • S. Houhou, S. Baarir, P. Poizat, Ph. Quéinnec, L. Kahloud : “A First-Order Logic Verification Framework for Communication-Parametric and Time-Aware BPMN Collaborations”, Information Systems, vol. 104, pp. 101765, (Elsevier) (2022)
• 2021
  • H. Xu, S. Baarir, T. Ziadi, L. Hillah, S. Essodaigui, Y. Bossu : “Optimisation for the product configuration system of Renault: towards an integration of symmetries”, 25^th ACM International Systems and Software Product Line Conference - Volume B, vol. B, SPLC '21: Proceedings of the 25^th ACM International Systems and Software Product Line Conference, Leicester, United Kingdom, pp. 86-90, (ACM) (2021)
  • S. Houhou, S. Baarir, P. Poizat, Ph. Quéinnec : “A Direct Formal Semantics for BPMN Time-Related Constructs”, ENASE 2021 - 16^th International Conference on Evaluation of Novel Approaches to Software Engineering, online, Czechia, pp. 138-149 (2021)
• 2020
  • V. Vallade, L. Le Frioux, S. Baarir, J. Sopena, V. Ganesh, F. Kordon : “Community and LBD-Based Clause Sharing Policy for Parallel SAT Solving”, SAT 2020 - 23^rd International Conference on Theory and Applications of Satisfiability Testing, vol. 12178, Lecture Notes in Computer Science, Alghero / Virtual, Italy, pp. 11-27 (2020)
  • Y. Amoussou‑Guenou, S. Baarir, M. Potop‑Butucaru, N. Sznajder, L. Tible, S. Tixeuil : “On the Encoding and Solving of Partial Information Games”, 8^th International Conference on Networked Systems (NETYS'20), Marrakech, Morocco (2020)
  • S. Tigane, L. Kahloul, S. Baarir, S. Bourekkache : “Dynamic GSPNs: formal definition, transformation towards GSPNs and formal verification”, EAI VALUETOOLS 2020 - 13^th EAI International Conference on Performance Evaluation Methodologies and Tools, Tsukuba, Japan (2020)
  • V. Vallade, L. Le Frioux, S. Baarir, J. Sopena, F. Kordon : “On the Usefulness of Clause Strengthening in Parallel SAT Solving”, NFM 2020 - 12^th NASA Formal Methods Symposium, Moffett Field / Virtual, United States (2020)
• 2019
  • S. Baarir : “Contributions to propositional satisfiability solving and its applications to the analysis of systems.”, habilitation, defence 06/19/2019 (2019)
  • S. Houhou, S. Baarir, P. Poizat, Ph. Quéinnec : “A First-Order Logic Semantics for Communication-Parametric BPMN Collaborations”, BPM 2019: Business Process Management, vol. 11675, Lecture Notes in Computer Science book series (LNCS), Vienna, Austria, pp. 52-68 (2019)
  • S. Tigane, L. Kahloul, S. Benharzallah, S. Baarir, S. Bourekkache : “Reconfigurable GSPNs: A modeling formalism of evolvable discrete-event systems”, Science of Computer Programming, vol. 183, pp. 102302, (Elsevier) (2019)
  • H. Metin, S. Baarir, F. Kordon : “Composing Symmetry Propagation and Effective Symmetry Breaking for SAT Solving”, NASA Formal Methods Symposium, vol. 11460, Lecture Notes in Computer Science, Houston, United States, pp. 316-332 (2019)
  • L. Le Frioux, S. Baarir, J. Sopena, F. Kordon : “Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework”, TACAS 2019 - 25^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 11427, Lecture Notes in Computer Science, Prague, Czechia, pp. 135-151 (2019)
• 2018
  • Y. Amoussou‑Guenou, S. Baarir, M. Potop‑Butucaru, N. Sznajder, L. Tible, S. Tixeuil : “On the encoding and solving partial information games”, (2018)
  • H. Metin, S. Baarir, M. Colange, F. Kordon : “CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving”, Tools and Algorithms for the Construction and Analysis of Systems 24^th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings,, Tessaloniki, Greece (2018)
  • S. Baarir, R. Bendraou, H. Metin, Y. Laurent : “ProVer: an SMT-based approach for process verification”, Model-Driven Engineering Verification & Validation, MoDELS Workshop, vol. 2245, MODELS Workshops, Copenhague, Denmark, pp. 555-562 (2018)
  • S. Tigane, L. Kahloul, S. Bourekkache, S. Baarir : “Extending GSPNs for the modelling, analysis and performance evaluation of dynamic systems”, International Journal of Critical Computer-Based Systems, vol. 8 (1), pp. 25, (Inderscience) (2018)
• 2017
  • L. Le Frioux, S. Baarir, J. Sopena, F. Kordon : “PaInleSS: a Framework for Parallel SAT Solving.”, The 20^th International Conference on Theory and Applications of Satisfiability Testing, vol. 10491, Lecture Notes in Computer Science, Melbourne, Australia, pp. 233-250, (Springer) (2017)
  • S. Baarir, K. Klai : “First international workshop on verification of business and software processes”, International Conference on Software and System Process, Paris, France, pp. 143-144, (ACM), (ISBN: 978-1-4503-5270-3) (2017)
  • T. Menouer, S. Baarir : “Parallel Learning Portfolio-based solvers”, International Conference On Computational Science, vol. 108, Elsevier Procedia Computer Science, Zürich, Switzerland, pp. 335-344 (2017)
  • T. Menouer, S. Baarir : “Parallel Satisfiability Solver Based on Hybrid Partitioning Method”, 25^th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, St. Petersburg, Russian Federation, pp. 54-60 (2017)
• 2015
  • D. Khelladi, R. Bendraou, S. Baarir, Y. Laurent, M.‑P. Gervais : “A Framework to Formally Verify Conformance of a Software Process to a Software Method”, 30^th ACM/SIGAPP Symposium On Applied Computing SAC, Salamanca, Spain, pp. 1518-1525, (ACM) (2015)
  • S. Baarir, A. Duret‑Lutz : “SAT-Based Minimization of Deterministic ω-Automata”, Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji, pp. 79-87 (2015)
• 2014
  • Y. Laurent, R. Bendraou, S. Baarir, M.‑P. Gervais : “Alloy4SPV : A Formal Framework for Software Process Verification”, ECMFA 2014 - 10^th European Conference on Modelling Foundations and Applications, vol. 8569, Lecture Notes in Computer Science, York, United Kingdom, pp. 83-100, (Springer) (2014)
  • Y. Laurent, R. Bendraou, S. Baarir, M.‑P. Gervais : “Formalization of fUML: An Application to Process Verification”, CAiSE 2014 - The 26^th International Conference on Advanced Information Systems Engineering, vol. 8484, Lecture Notes in Computer Science, Thessaloniki, Greece, pp. 347-363, (Springer) (2014)
  • S. Baarir, A. Duret‑Lutz : “Mechanizing the Minimization of Deterministic Generalized Büchi Automata”, Formal Techniques for Distributed Objects, Components, and Systems, vol. 8461, Lecture Notes in Computer Science, Berlin, Germany, pp. 266-283, (Springer) (2014)
  • Y. Laurent, R. Bendraou, S. Baarir, M.‑P. Gervais : “Planning for Declarative Processes”, SAC'14 - The 29^th Annual ACM Symposium on Applied Computing, Gyeongju, Korea, Republic of, pp. 1126-1133, (ACM) (2014)
• 2013
  • M. Colange, S. Baarir, F. Kordon, Y. Thierry‑Mieg : “Towards Distributed Software Model-Checking using Decision Diagrams”, 25^th International Conference on Computer Aided Verification (CAV), vol. 8044, Lecture Notes in Computer Science, Saint-Petersbourg, Russian Federation, pp. 830-845, (Springer Verlag) (2013)
• 2012
  • S. Baarir, F. Kordon : “Modeling and Verifying Distributed Systems with Petri Nets (tutorial)”, 2^nd IEEE International Workshop on Advanced Information Systems for Enterprises (IWAISE), Constantine, Algeria, pp. 92-92, (IEEE Press) (2012)
  • M. Colange, F. Kordon, Y. Thierry‑Mieg, S. Baarir : “State Space Analysis using Symmetries on Decision Diagrams”, 12^th International Conference on Application of Concurrency to System Design (ACSD'2012), Hamburg, Germany, pp. 164-172, (IEEE Computer Society) (2012)
• 2011
  • S. Baarir, C. Braunstein, E. Encrenaz, J.‑M. Ilié, I. Mounier, D. Poitrenaud, S. Younes : “Feasibility Analysis for Robustness Quantification by Symbolic Model Checking”, Formal Methods in System Design, vol. 39 (2), pp. 165-184, (Springer Verlag) (2011)
  • M. Colange, S. Baarir, F. Kordon, Y. Thierry‑Mieg : “Crocodile: a Symbolic/Symbolic tool for the analysis of Symmetric Nets with Bag”, 32^nd International Conference on Petri Nets and Other Models of Concurrency (ICATPN 2011), vol. 6709, Lecture Notes in Computer Science, Newcastle, United Kingdom, pp. 338-347, (Springer) (2011)
  • S. Baarir, M. Beccuti, C. Dutheillet, G. Franceschinis, S. Haddad : “Lumping partially symmetrical stochastic models”, Performance Evaluation, vol. 68 (1), pp. 21-44, (Elsevier) (2011)
• 2010
  • S. Baarir, C. Braunstein, E. Encrenaz, J.‑M. Ilié, T. Li, I. Mounier, D. Poitrenaud, S. Younes : “Quantifying Robustness by Symbolic Model checking”, 1^st Hardware Verification Workshop (CAV workshop), Edinburgh, United Kingdom, pp. 1-12 (2010)
  • S. Baarir, L. Hillah, F. Kordon, E. Renault : “Self-Reconfigurable Modular Robots and their Symbolic Configuration Space”, Modeling, Development and Verification of Adaptative Computer Systems: the Grand Challenge for Robust Software, 16^th Monterey Workshop 2010, Redmond, Revised Selected Papers, vol. 6662, Lecture Notes in Computer Science, Redmond, United States, pp. 103-121, (Springer) (2010)
• 2009
  • S. Baarir, M. Beccuti, C. Dutheillet, G. Franceschinis : “From partially to fully lumped Markov chains in Stochastic Well Formed Petri Nets”, Proc. 4^th International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS), Pisa, Italy, pp. 43:1-43:10, (ICST) (2009)
  • S. Baarir, M. Beccuti, D. Cerotti, M. De Pierro, S. Donatelli, G. Franceschinis : “The GreatSPN Tool: Recent Enhancements”, ACM SIGMETRICS Performance Evaluation Review, vol. 36 (4), pp. 4-9, (Association for Computing Machinery) (2009)
  • S. Baarir, C. Braunstein, R. Clavel, E. Encrenaz, J.‑M. Ilié, R. Leveugle, I. Mounier, L. Pierre, D. Poitrenaud : “Complementary formal approaches for dependability analysis”, The 24^th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, Chicago, Illinois, United States, pp. 331-339, (IEEE Computer Society) (2009)
  • J. Sopena, S. Baarir, F. Legond‑Aubry : “Vérification formelle d’un algorithme générique et hiérarchique d’exclusion mutuelle”, Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, vol. 28 (9), pp. 1085-1105, (Lavoisier) (2009)
• 2008
  • S. Baarir, J. Sopena, F. Legond‑Aubry : “On the Formal Verification of a Generic Hierarchical Mutual Exclusion Algorithm”, 28^th IFIP International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'08 ), vol. 5048, Lecture Notes in Computer Science, Tokyo, Japan, pp. 99-115, (Springer-Verlag) (2008)
• 2007
  • S. Baarir : “Exploitation des symétries partielles pour la vérification et l’évaluation de performances des systèmes concurrents”, thesis, defence 05/16/2007, supervision Haddad, Serge, co-supervision : Ilié, Jean-Michel, Dutheillet, Claude (2007)
  • S. Baarir, A. Duret‑Lutz : “Test de vacuité pour automates de Büchi ensemblistes avec tests d’inclusion”, 6^e Colloque Francophone sur la Modélisation des Systèmes Réactifs (MSR'07), Lyon, France, pp. 19-34, (Hermes-Lavoisier) (2007)
  • S. Baarir, A. Duret‑Lutz : “Emptiness Check of Powerset Buchi Automata”, 7^th International Conference on Application of Concurrency to System Design (ACSD'07), Bratislava, Slovakia, pp. 41-50, (IEEE) (2007)
• 2006
  • S. Baarir, A. Duret‑Lutz : “Emptiness Check of Powerset Büchi Automata using Inclusion Tests”, (2006)
  • M. Beccuti, S. Baarir, G. Franceschinis, J.‑M. Ilié : “Efficient Lumpability Check in Partially Symmetric Systems”, 3^rd International Conference on the Quantitative Evaluation of Systems (QEST '06), Riverside, CA, United States, pp. 211-220, (IEEE Computer Society) (2006)
  • J.‑M. Ilié, Y. Thierry‑Mieg, S. Baarir : “Vérification efficace des systèmes finis”, chapitre de Méthodes Formelles pour les Systèmes Répartis et Coopératifs, Traités IC2 - Informatique et systèmes d'information, pp. 171-211, (Hermes-Lavoisier), (ISBN: 2-7462-1447-4) (2006)
• 2005
  • S. Baarir, C. Dutheillet, S. Haddad, J.‑M. Ilié : “On the Use of Exact Lumpability in Partially Symmetrical Well-Formed Nets”, 2^nd International Conference on the Quantitative Evaluation of Systems (QEST '05), Torino, Italy, pp. 23-32, (IEEE Computer Society Press) (2005)
• 2004
  • S. Baarir, J.‑M. Ilié, A. Duret‑Lutz : “Improving Reachability Analysis for Partially Symmetric High Level Petri Nets”, 12^th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS '04), Volendam, Netherlands, pp. 5-8 (2004)
  • S. Baarir, S. Haddad, J.‑M. Ilié : “Exploiting Partial Symmetries in Well-formed nets for the Reachability and the linear Time Model Checking Problems”, 7^th Workshop on Discrete Event Systems (WODES '04), Reims, France, pp. 223-228 (2004)
  • J. Hugues, Y. Thierry‑Mieg, F. Kordon, L. Pautet, S. Baarir, Th. Vergnaud : “On the Formal Verification of Middleware Behavioral Properties”, 9^th International Workshop on Formal Methods for Industrial Critical Systems (FMICS '04), Linz, Austria, pp. 139-157, (Elsevier) (2004)
  • J.‑M. Ilié, S. Baarir, M. Beccuti, C. Delamare, S. Donatelli, C. Dutheillet, G. Franceschinis, R. Gaeta, P. Moreaux : “Extended SWN Solvers in GreatSPN”, 1^st International Conference on Quantitative Evaluation of Systems (QEST '04), Enschede, Netherlands, pp. 324-325, (IEEE Computer Society) (2004)
  • Y. Thierry‑Mieg, S. Baarir, A. Duret‑Lutz, F. Kordon : “Nouvelles techniques de Model Checking pour la vérification de systèmes complexes”, Génie logiciel : le magazine de l'ingénierie du logiciel et des systèmes, vol. 69, pp. 17-23, (Génie industriel multimédia) (2004)