Direction de recherche : Fabrice KORDON

Co-encadrement : DURET-LUTZ Alexandre, POITRENAUD Denis

Contribution aux tests de vacuité pour le model checking explicite

L'approche automate pour le model checking de propriétés temporelles à temps linéaire est une technique classique de vérification formelle de systèmes concurrents. Un système, ainsi qu'une propriété qu'on souhaite y vérifier, sont modélisés sous forme d’omega-automates reconnaissant des mots infinis. Des manipulations de ces automates (produit synchronisé et test de vacuité) permettent d'établir si le système vérifie la propriété ou non.
Dans cette thèse nous nous focalisons sur un type particulier d'omega-automates qui permettent une représentation concise des propriétés d'équité faible: les automates de Büchi généralisés basés sur les transitions (Transition-based Generalized Büchi Automata).
Dans un premier temps, nous brossons un aperçu des algorithmes de vérification existant et nous en proposons de nouveaux traitant efficacement les automates généralisés forts. Dans un second temps, l'analyse des composantes fortement connexes de l'automate de la propriété nous a conduit à élaborer une décomposition de cet automate. Cette décomposition se focalise sur les automates multi-forces et permet une parallélisation naturelle des model-checkers. Enfin, nous avons proposé les premiers tests de vacuité parallèles pour les automates généralisés. De plus, tous ces tests sont lock-free à la différence de ceux de l’état de l’art. Toutes ces techniques ont ensuite été implémentées et évaluées sur un jeu de test conséquent.

Publications 2010-2023

• 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)
• 2022
  • E. Paviot‑Adet, D. Poitrenaud, E. Renault, Y. Thierry‑Mieg : “LTL under reductions with weaker conditions than stutter-invariance”, Lecture Notes in Computer Science (LNCS), vol. 13273, Formal Techniques for Distributed Objects, Components, and Systems, Lucca, Italy, pp. 170–187, (Springer Cham), (ISBN: 978-3-031-08679-3) (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)
• 2019
  • D. Poitrenaud, E. Renault : “Combining Parallel Emptiness Checks with Partial Order Reductions”, ICFEM 2019 - 21^st International Conference on Formal Engineering Methods, vol. 11852, Lecture Notes in Computer Science, Shenzhen, China, pp. 370-386, (Springer) (2019)
• 2017
  • E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Variations on Parallel Explicit Emptiness Checks for Generalized Büchi Automata”, International Journal on Software Tools for Technology Transfer, vol. 19 (6), pp. 653-673, (Springer Verlag) (2017)
• 2016
  • A. Duret‑Lutz, F. Kordon, D. Poitrenaud, E. Renault : “Heuristics for Checking Liveness Properties with Partial Order Reductions”, Automated Technology for Verification and Analysis, vol. 9938, Lecture Notes in Computer Science, Chiba, Japan, pp. 340-356, (Springer) (2016)
• 2015
  • E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Parallel Explicit Model Checking for Generalized Büchi Automata”, 21^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015, vol. 9035, Lecture Notes in Computer Science, London, United Kingdom, pp. 613-627, (Springer) (2015)
• 2014
  • E. Renault : “Contribution aux tests de vacuité pour le model checking explicite”, soutenance de thèse, soutenance 05/12/2014, direction de recherche Kordon, Fabrice, co-encadrement : Duret-lutz, Alexandre, Poitrenaud, Denis (2014)
• 2013
  • E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Three SCC-based Emptiness Checks for Generalized Büchi Automata”, Proceedings of the 19^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'13), vol. 8312, Lecture Notes in Computer Science, Stellenbosch, South Africa, pp. 668-682, (Springer) (2013)
  • E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking”, Proceedings of the 19^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), vol. 7795, Lecture Notes in Computer Science, Rome, Italy, pp. 580-593, (Springer) (2013)
• 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)