Homepage of Etienne Renault

During my PhD I worked on the emptiness checks for explicit model checking. This work focused especially on generalized Büchi automata that support weak fairness hypothesis. During this thesis, I proposed several parallel or sequential emptiness checks. My work also lead me to explore the property automaton to reduce the complexity of emptiness check.

Actually, I work at the LRDE lab around SPOT which is a model checking library based on TGBA (Transition-based Generalized Büchi Automata). My research interest are more generally oriented to formal methods and its applications.

If you want a quick look at all my publications you can look my DPLB page; for more information see below :

• SPIN21 (slides) (BibTex)

  Go2Pins: a framework for the LTL verification of Go programs

• ISSE20 (BibTex)

  Improving Swarming Using Genetic Algorithms

• ICFEM19 (slides) (BibTex) benchmark

  Combining Parallel Emptiness Checks with Partial Order Reductions

• VECoS18 (slides) (BibTeX) benchmark

  Improving Parallel State-Space Exploration Using Genetic Algorithms

• HPCR18 (BibTeX)

  Parallel Model Checking Algorithms for Linear-time Temporal Logic

• ATVA16 (slides) (BibTeX) benchmark

  Heuristics for Checking Liveness Properties with Partial Order Reductions

• ATVA16 (short paper) (slides) (BibTex)

  Spot 2.0 — a framework for {LTL} and ω-automata manipulation

• STTT16 (BibTeX) benchmark

  Variations on Parallel Explicit Model Checking for Generalized Büchi Automata

• TACAS15 (extented version with proof in appendix) (slides) (BibTeX) benchmark

  Parallel Explicit Model Checking for Generalized Büchi Automata

• My PhD dissertation, slides and data can be found here (bibtex)

• LPAR13 (bibtex) (slides) benchmark

  Three SCC-based Emptiness Checks for Generalized Büchi Automata

• TACAS 2013 (BibTeX) benchmark

  Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking

• Monterey Workshop 2010 (BibTeX)

  Self-reconfigurable Modular Robots and Their Symbolic Configuration Space

• The Quest For An Efficient Model-Checking at MeFoSyLoMa

(2017-…) Distributed Systems (ALGOREP) here

(2017-…) Literature Review (BIBLIO) here

(2016-…) Programming languages comparison Lecture (TYLA) here

(2015-…) Compilation Lecture (CMP1/CMP2) here

(2015-…) Introduction to Model-Checking (IMC) here

(2015) An overview of Android here! and more here! and here! (in French)

(2014-…) Introduction to algorithms and data structures (ALGA) here and here

(2014-…) Management of the Tiger project at EPITA.

(2014) An overview of Android here! (in French)

(2013) An overview of Android here! (in French)

GNU Emacs Reference toward the emacs manual

Org Mode Manual Reference toward the org mode manual, which is an emacs mode used to create this website.