Supervision : Fabrice KORDON

Co-supervision : DURET-LUTZ Alexandre, POITRENAUD Denis

Contribution aux tests de vacuité pour le model checking explicite

The automata-theoretic approach to linear time model-checking is a standard technique for formal verification of concurrent systems. The system and the property to check are modeled with omega-automata that recognizes infinite words. Operations overs these automata (synchronized product and emptiness checks) allows to determine whether the system satisfies the property or not.
In this thesis we focus on a particular type of omega-automata that enable a concise representation of weak fairness properties: transitions-based generalized Büchi automata (TGBA).
First we outline existing verification algorithms, and we propose new efficient algorithms for strong automata. In a second step, the analysis of the strongly connected components of the property automaton led us to develop a decomposition of this automata. This decomposition focuses on multi-strength property automata and allows a natural parallelization for already existing model-checkers. Finally, we proposed, for the first time, new parallel emptiness checks for generalized Büchi automata. Moreover, all these emptiness checks are lock-free, unlike those of the state-of-the-art. All these techniques have been implemented and then evaluated on a large benchmark.

1 PhD student (Supervision / Co-supervision)

• KHEIREDDINE Anissa : Parallélisation et optimisation du Bounded model-checking

2010-2022 Publications

• 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)
• 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”, thesis, defence 12/05/2014, supervision Kordon, Fabrice, co-supervision : 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)