Supervision : Serge HADDAD

Co-supervision : ILIÉ Jean-Michel, DUTHEILLET Claude

Exploitation des symétries partielles pour la vérification et l'évaluation de performances des systèmes concurrents

Le travail présenté dans cette thèse s'intéresse à la réduction de l'explosion combinatoire rencontrée lors de la vérification formelle par model-checking ou l'évaluation de performances de systèmes concurrents finis. L'approche suivie pour obtenir cette réduction consiste à combattre l'explosion combinatoire à la source en mettant à profit les symétries pouvant apparaître dans les systèmes analysés et ainsi pouvoir factoriser la représentation de ces comportements. La contribution apportée par ce travail consiste à prendre en compte les symétries partielles. Il apporte des solutions originales en proposant une séparation entre les parties symétriques et asymétriques du comportement, permettant la construction d'un espace d'état quotient dans lequel les symétries sont évaluées dynamiquement au cours du processus de vérification ou d'évaluation.

Two PhD students (Supervision / Co-supervision)

Six past PhD students (2013 - 2023) at Sorbonne University

2004-2024 Publications

• 2024
  • H. Xu, S. Baarir, T. Ziadi, S. Essodaigui, Y. Bossu : “Automated Parameter Determination for Enhancing the Product Configuration System of Renault: An experience report”, 28^th International Conference on Engineering of Complex Computer Systems (ICECCS 2024), Limassol, Cyprus (2024)
  • S. Saouli, S. Baarir, C. Dutheillet : “Tackling the Polarity Initialization Problem in SAT Solving Using a Genetic Algorithm”, 16^th International Symposium, NFM 2024Moffett Field, CA, USA, June 4–6, 2024Proceedings, vol. 14627, Lecture Notes in Computer Science, Moffett Field, CA, United States, pp. 21-36, (Springer Nature Switzerland) (2024)
• 2023
  • H. Xu, S. Baarir, T. Ziadi, S. Essodaigui, Y. Bossu, L. Hillah : “An Experience Report on the Optimization of the Product Configuration System of Renault *”, 2023 27^th International Conference on Engineering of Complex Computer Systems (ICECCS), Toulouse, France, pp. 197-206, (IEEE), (ISBN: 979-8-3503-4004-4) (2023)
  • H. Xu, S. Baarir, T. Ziadi, S. Essodaigui, Y. Bossu, L. Messan Hillah : “Optimization of the Product Configuration System of Renault”, SAC '23: 38^th ACM/SIGAPP Symposium on Applied Computing, SAC '23, Tallinn, Estonia, pp. 1486-1489, (ACM), (ISBN: 9781450395175) (2023)
  • A. Kheireddine, E. Renault, S. Baarir : “Towards Better Heuristics for Solving Bounded Model Checking Problems”, Constraints, vol. 28, pp. 45-66, (Springer Verlag) (2023)
  • S. Saouli, S. Baarir, C. Dutheillet, J. Devriendt : “CosySEL: Improving SAT Solving Using Local Symmetries”, Verification, Model Checking, and Abstract Interpretation, vol. 13881, Lecture Notes in Computer Science, Boston (MA), United States, pp. 252-266, (Springer Nature Switzerland) (2023)
• 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)
  • A. Kheireddine, E. Renault, S. Baarir : “Tuning SAT Solvers for LTL Model Checking”, 2022 29^th Asia-Pacific Software Engineering Conference (APSEC), virtual event, Japan, pp. 259-268, (IEEE), (ISBN: 978-1-6654-5537-4) (2022)
• 2021
  • A. Kheireddine, E. Renault, S. Baarir : “Towards Better Heuristics for Solving Bounded Model Checking Problems”, 27^th International Conference on Principles and Practice of Constraint Programming (CP 2021), vol. 210, Leibniz International Proceedings in Informatics (LIPIcs), Montpellier (Virtual Conference), France, pp. 7:1-7:11, (Schloss Dagstuhl − Leibniz-Zentrum für Informatik), (ISBN: 978-3-95977-211-2) (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)
  • Y. Amoussou‑Guenou, S. Baarir, M. Potop‑Butucaru, N. Sznajder, L. Tible, S. Tixeuil : “On the Encoding and Solving of Partial Information Games”, Networked Systems, vol. 12129, Lecture Notes in Computer Science, Marrakech, Morocco, pp. 60-76, (Springer International Publishing), (ISBN: 978-3-030-67087-0) (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)
  • 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, phd 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, phd 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)