Research
My research is about computer-aided verification and synthesis techniques for critical systems. This field studies the methods that allow to automatically prove that a computer system is correct (i.e. without bugs), or to automatically build computer systems that are correct with respect to a given specification. I have been involved in the development of the following tools/projects:
- The Babylon project
- The Expand, Enlarge and Check algorithm (for the safety properties of WSTS).
- The CSC tool for the computation of the coverability set of Petri nets
- The LavaBDD library implementing the LVBDD datastructure
Students:
- PhD student (current): Morgane Estiévenart (UMons), Markus Lindström
- Master students (current): B. Adhikari, S. De Baets, L. Delauvaux (UMons), F. Fragapane (UMons), P. Hiep Tuan, Q. Vin Pham
- Master students (past): M. Duchêne (2011), R. Akgun (2011), Y. Ben Abdelkader (2011), M. Ciullo (Umons, 2011), G. Graziano (Umons, 2011), F. Kichaout (2011), O. Muhizi Alvin (UMons, 2010), H. Yavuz (UMons, 2010), S. Lukitcheva (2010).
You can also have a look at my list of publications. Drag your mouse above the titles to read the abstracts:
Recent and submitted works
Multiprocessor Schedulability of Arbitrary-Deadline Sporadic Tasks: Complexity and Antichain Algorithm (with Joël Goossens and Markus Lindström). Invited journal version of the RTNS 2011 paper. Under review. [BibTex] [PDF file, 4,4 Mb].
Queue-Dispatch Asynchronous Systems (with Alexander Heußner and Jean-François Raskin). Submitted. [BibTex] [PDF file, ArXiv.org].
Journal papers
On the efficient computation of the coverability set for Petri nets (invited journal version of the ATVA07 paper) (with Jean-François Raskin and Laurent Van Begin). International Journal of Foundations of Computer Science, 21(2), 2010, World Scientific Publishing Company. [PDF file, 309 Kb] [BibTex] [DOI]. Published version is (c) WSPC.
Le problème de couverture pour les réseaux de Petri: résultats classiques et développements récents (in French) (with Pierre Ganty, Jean-François Raskin and Laurent Van Begin). Techniques et Sciences Informatique, 29(2), Lavoisier, 2010. [PDF file, 289 Kb] [BibTeX] [DOI].
Well-structured Languages (with Jean-François Raskin and Laurent Van Begin). Acta Informatica, volume 44(3-4), pp 249-288, Springer, 2007. [PDF file, full version, 388 Kb] [BibTex] [DOI]. The original publication is available on springerlink.com
Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS (with Jean-François Raskin and Laurent Van Begin). Journal of Computer and System Sciences, volume 72(1), pp 180-203, Elsevier, 2005. [PDF file, full version, 326 Kb] [BibTeX] [DOI]. Published version is (c) Elsevier Publishing.
On the omega-language expressive power of extended Petri nets (with Alain Finkel, Jean-François Raskin and Laurent Van Begin). Theoretical Computer Science, volume 356(3), pp 374-386, Elsevier, 2006. [PDF file, full version 190 Kb] [BibTeX] [DOI]. Published version is (c) Elsevier Publishing.
Conference Proceedings and Technical reports
A faster exact multiprocessor schedulability test for sporadic tasks (with Joël Goossens and Markus Lindström). In the proceedings of RTNS 2011. Best student paper award. [BibTex] [PDF file, ArXiv.org].
Event-clock automata: form theory to practice (with Jean-François Raskin an Tali Sznajder). In the proceedings of FORMATS 2011, Lecture Notes in Computer Science 6919, Springer, 2011. [BibTex] [DOI] [PDF file, ArXiv.org].The original publication is available on springerlink.com.
On reachability for hybrid automata over bounded time (with Thomas Brihaye, Laurent Doyen, Joël Ouaknine, Jean-François Raskin and James Worrell). In the proceedings of ICALP 2011 ICALP 2011, Lecture Notes in Computer Science 6756, Springer Verlag. [BibTex] [PDF file, ArXiv.org] [DOI]. The original publication is available on springerlink.com
Safraless procedures for timed specifications (with Barbara di Giampaolo, Tali Sznajder and Jean-François Raskin). In the Proceedings of FORMATS 2010 (invited paper), Lecture Notes in Computer Science 6246, Springer Verlag. [BibTex] [PDF file, 481 Kb] [DOI]. The original publication is available on springerlink.com
Lattice-Valued Binary Decision Diagrams (with Gabrial Kalyon, Tristan Le Gall, Nicolas Maquet and Jean-François Raskin). In the Proceedings of ATVA 2010, Lecture Notes in Computer Science, volume 6252, Springer Verlag. [BibTex] [PDF file, 701 Kb] [DOI] The original publication is available on springerlink.com.
Realizability of Real-Time Logics (with Laurent Doyen, Jean-François Raskin and Julien Reichert). In the proceedings of FORMATS09, Lecture Notes in Computer Science, volume 5813, pages 133-148, Springer Verlag. [BibTex] [PDF file, 204 Kb] [DOI]. The original publication is available on springerlink.com
On the expressive power of Petri nets with transfer arcs vs. Petri nets with reset arcs. Technical report 572, ULB. [BibTex] [PDF file, 147 Kb].
On the efficient Computation of the Minimal Coverability set of Petri nets (with Jean-François Raskin and Laurent Van Begin). In the Proceedings of ATVA07, Lecture Notes in Computer Science, volume 4762, pages 98-113, Springer Verlag. [BibTex] [PDF file, 238 Kb] [DOI]. The original publication is available on springerlink.com
Expand, Enlarge and Check... Made Efficient (with Jean-François Raskin and Laurent Van Begin), in the Proceedings of. CAV'05, Lecture Notes in Computer Science, volume 3576, pages 394-407 Springer Verlag. [BibTex] [PDF file, 244 Kb] [DOI]. The original publication is available on springerlink.com
A counter-example to the minimal coverability tree algorithm (with Alain Finkel, Jean-François Raskin and Laurent Van Begin), Technical report 535, ULB. [BibTex] [PDF file, 90 Kb].
Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS (with Jean-François Raskin and Laurent Van Begin). In the Proceedings of FSTTCS 2004, Lecture Notes in Computer Science, volume 3328, pages 287--298. Springer-Verlag, 2004. [BibTeX]. Full paper (with all the proofs): [PDF file, 337 Kb] [DOI]. The original publication is available on springerlink.com
On the omega-language expressive power of extended Petri nets (with Alain Finkel, Jean-François Raskin and Laurent Van Begin). In the Proceedings of EXPRESS'04, Electronic Notes in Computer Sciences, 128(2), pp 87-101, Elsevier, 2005. Pre-print version [PDF file, 305 Kb]. The proceedings version (c) Elsevier is available on Science Direct. The proofs are available in the journal version of the paper (see above). [BibTeX]. Also Technical Report 519, ULB, 2004.
Concurrent Boolean Programs (with Laurent Van Begin), Technical Report 505, ULB, 2003. [Postscript file, 583 Kb] [BibTeX]
Babylon: An integrated toolkit for the specification and verification of parameterized systems (with Pierluigi Ammirati, Giorgio Delzanno, Pierre Ganty, Jean-François Raskin and Laurent Van Begin). In the Proceedings of SAVE, 2002 [PostScript file, 184 Kb] [BibTeX entry].
Dissertations
Coverability and Expressiveness Properties of Well-structured Transitions Systems, PhD thesis, ULB, 2007. [PDF file, 2.1 Mb]. Slides for the FRS/FNRS IBM award: [PDF file, 3,8 Mb]
How to grind Java software to extract full-bodied infinite-state models ?, Diplome d'études approfondies, ULB, 2003. [PDF file 1.4 Mb] [Bibtex Entry] [Slides of the presentation, PDF, 1.4 Mb].
A comparison of various backward analyzers for parametrized concurrent systems, Master's thesis, ULB, 2002. [PS.GZ file, 417 Kb] [Slides of the presentation, PDF] [Bibtex Entry].
Some material related to this work:
- Link to the grammar of the input language of the tools.
- Detail of the classes of Yaba.
- Some guidelines to integrate a new datastructure in Babylon.
Photo: L. Geeraerts