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.

Current research projects:

   FORESt    SyVeRLo
PDR FNRS - FORESt:
Formal verificatiOn techniques for REal-time Scheduling problems
PDR FNRS - SyVeRLo:
Synthesis and Verification of Real-time Logics

Past research projects:

  
FP7 - CASSTING:
Collaborative Adaptive Systems SynThesIs using Non-zero sum Games

I have been involved in the development of the following tools/projects:

Current students:

  • Post Docs: Ho Hsi-Ming (UMons), Van-Anh Nguyen.
  • PhD student: Marion Hallet (co-supervision ULB,UMONS)
  • Intern: Aline Goeminne (UMONS).
  • Master students: Gabriel Shako Ekanga.

Past students:

  • Post Docs: Amit Kumar Dhar (now Assistant Professor at IIIT Allahabad, India), Axel Haddad (UMons), Pritha Mahata, Benjamin Monmege (now Associate Professor at Aix-Marseille University), Gabriel Renault (UMONS), Amélie Stainer
  • PhD students: Morgane Estiévenart (PhD UMONS, 2015), Markus Lindström
  • Interns : E. Lefaucheux (ENS Cachan, 2014-2015), P.  Jensen (2013, U. Aalborg), J.  Taankvist (2013, U. Aalborg).
  • Master students : O. Svoboda (2016), G. Talla (2016), S. Picard (2016), S Dehouck (2015), A. Lebeau (2014), J. Meulemans (2014), M. Fontaine (2013), J. Stilmant (2013), B. Adhikari (2012), S. De Baets (2012), F. Fragapane (UMons, 2012), T. Phan Hiep (2012), P. Quang Vin (2012), 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).

My profile on Google Scholar and my entry on DBLP.

My publications (drag your move above the title to read the abstract):

Recent and submitted works

A Game-Based Algorithm for the Multiprocessor Online Feasibility of Sporadic Tasks (with Joël Goossens and Van-Anh Nguyen). Submitted, 2016. [PDF file, 418Kb].

Synthesising Succinct Strategies in Safety Games with an Application to Real-time Scheduling (with Joël Goossens, Thi-Van-Anh Nguyen and Amélie Stainer). Submitted, 2015. [PDF file, 1.2Mb].

Journal papers

Pseudopolynomial Iterative Algorithm to Solve Total-Payoff Games and Min-Cost Reachability Games (with Thomas Brihaye, Axel Haddad and Benjamin Monmege). Accepted for publication in a special issue of Acta Informatica. To appear, 2016. [PDF file, 558Kb] [DOI].

On the Verification of Concurrent, Asynchronous Programs with Waiting Queues (with Alexander Heußner and Jean-François Raskin). In ACM Transactions on Embedded Computing, 14(3), 2015. [BibTex] [DOI] [PDF file, 1 Mb].

ω-Petri nets: algorithms and complexity (with Alexander Heußner, M. Praveen and Jean-François Raskin). In Fundamenta Informaticæ 137:29-60, 2015. [BibTex] [DOI] [PDF file, 504 kB].

On regions and zones for event-clock automata (with Jean-François Raskin and Nathalie Sznajder). In Formal Methods in Systems Design, 45(3), Springer, 2014. [BibTex] [DOI] [PDF file, 424 kB].

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. Real-Time Systems, The International Journal of Time-Critical Computing Systems, volume 49(2), pp 171-218, Springer, 2013. [BibTex] [DOI] [PDF file, 615 kB]. The original publication is available on springerlink.com

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, volume 21(2), World Scientific Publishing Company, 2010. [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

Real-time Synthesis is Hard! (with Thomas Brihaye, Morgane Estiévenart, Hsi-Ming Ho, Benjamin Monmege and Tali Sznajder). Accepted for publication in the proceedings of FORMATS 2016, to appear, 2016. [PDF file, arXiv.org]

Efficient Energy Distribution in a Smart Grid using Multi-Player Games (with Thomas Brihaye, Amit Kumar Dhar, Axel Haddad and Benjamin Monmege). In the proceedings of the CASSTING'16 workshop at ETAPS, EPTCS 220, 2016. [PDF file, 135Kb] [DOI].

Simple Priced Timed Games are not That Simple  (with Thomas Brihaye, Axel Haddad, Engel Lefaucheux and Benjamin Monmege). To appear in the proceedings of FSTTCS 2015, LIPIcs vol. 45, Schloß Dagstuhl. [PDF full version, arXiv.org] [DOI].

Quantitative Games under Failures  (with Thomas Brihaye, Axel Haddad, Guillermo A. Pérez, Benjamin Monmege and Gabriel Renault). To appear in the proceedings of FSTTCS 2015, LIPIcs vol. 45, Schloß Dagstuhl. Full version: [PDF full version, arXiv.org] [DOI].

To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games  (with Thomas Brihaye, Axel Haddad and Benjamin Monmege). In the proceedings of CONCUR 2015. LIPIcs, vol. 42, Schloß Dagstuhl, 2015. [PDF full version, arXiv.org] [DOI].

Synthesising Succinct Strategies in Safety Games (with Joël Goossens and Amélie Stainer). In the proceedings of RP 2014. Lecture Notes in Computer Science 8762, Springer, 2014 [PDF file, arXiv.org] [DOI]. The original publication is available on springerlink.com.

On MITL and alternating timed automata over infinite words (with Thomas Brihaye and Morgane Estiévenart). In the proceedings of FORMATS 2014. Lecture Notes in Computer Science 8711, Springer, 2014. [BibTex] [PDF file, arXiv.org] [DOI]. The original publication is available on springerlink.com.

Adding Negative Prices to Priced Timed Games (with Thomas Brihaye, Shankara Narayanan Krishna, Lakshmi Manasa, Benjamin Monmege, and Ashutosh Trivedi). In the proceedings of CONCUR 2014. Lecture Notes in Computer Science 8704, Springer, 2014.[BibTex] [PDF file, arXiv.org] [DOI]. The original publication is available on springerlink.com.

Time-bounded Reachability for Hybrid Automata: Complexity and Fixpoints (with Thomas Brihaye, Laurent Doyen, Joël Ouaknine, Jean-François Raskin and James Worrell) In the proceedings of ATVA2013. Lecture Notes in Computer Science 8172, Springer, 2013.[BibTex] [PDF file, arXiv.org] [DOI]. The original publication is available on springerlink.com

On MITL and alternating timed automata (with Thomas Brihaye and Morgane Estiévenart). In the proceedings of FORMATS 2013, Lecture Notes in Computer Science 8053, Springer, 2013. [BibTex] [PDF file, arXiv.org] [DOI]. The original publication is available on springerlink.com

ω-Petri nets (with Alexander Heußner, M. Praveen and Jean-François Raskin). In the proceedings of Petri Nets 2013, Lecture Notes in Computer Science 7927, Springer, 2013. [BibTex] [PDF file, arXiv.org] [DOI]. The original publication is available on springerlink.com

Queue-Dispatch Asynchronous Systems (with Alexander Heußner and Jean-François Raskin). In the proceedings of ACSD 2013, IEEE. [BibTex] [PDF file, arXiv.org] [DOI].

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] [DOI]. 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:

Teaching (Enseignement)

J'enseigne les cours suivants:

Par le passé, j'ai participé aux enseignements suivants:

  • Analysis of Petri nets: Course about Petri nets, parts of a series of tutorials in the MoVES IAP project [Web Page] [Slides, PDF, 3.9 Mb].
  • Collège Belgique: les problèmes indécidables
  • Introduction à l'Algorithmique (Année préparatoire au Master en cours du soir - UMons): Page officielle du cours.
  • INFO-F-402 Computability and complexity
  • Langages de Programmation 1 Téléchargez les transparents du cours (C++): [Fichier PDF, 4,2 Mo]

Links

  • Miss chipote: My mother's blog about embroidery, sewing, craftworks. I am the computer scientist, she has a blog, I haven't. Don't ask why...
  • Chabazz: My wife has a blog too !
  • But I have a flickr ! Analog photographs made with vintage cameras (one of them is 80 years old...)

Contact

You can contact me by

  • E-mail: gigeerae [at] ulb.ac.be
  • Phone: +32 2 650 55 96
  • Snail Mail:
    Gilles GEERAERTS
    Université libre de Bruxelles
    Campus de la Plaine
    Département d’Informatique, CPI 212
    Boulevard du Triomphe
    B - 1050 Bruxelles
    BELGIUM
You can get my GPG key here.