Formal Methods and Verification at ULB   Computer Science Department at ULB  

Nicolas Maquet

NOTICE
This page is out of date.
I obtained my Ph.D. in March 2011 and have since left the ULB.

I obtained a Master's Degree in Computer Science here at ULB in 2006. Since then, I have been working in the research team of Jean-François Raskin, part of the Formal Methods and Verification Group at ULB. From January to October 2007, my research activity was financed by the Interuniversity Attraction Poles (IAP) of the Belgian Science Policy. Since October 2007, I work under a FRIA (an associated fund of the FNRS) research grant.
My research interests include automata theory, verification of reactive systems, model checking, temporal logic, real-time and embedded systems and provably-correct code generation.


Nicolas Maquet
Contact - Research - Links
Contact


  • Office : 2.N8.207
  • Address :
    University of Brussels (ULB),
    Computer Science Department,
    Campus de la Plaine - CP 212,
    Boulevard du Triomphe - B-1050 Brussels.
  • Phone : +32 (0)2 650 55 95
  • Email : nmaquet (AT SIGN HERE) ulb.ac.be
  • GPG public key
Research

Publications

  • New Algorithms and Data Structures for the Emptiness Problem of Alternating Automata (Ph.D. thesis) [ PDF ]
  • Lattice-Valued Binary Decision Diagrams [ PDF ]
  • Fixpoint Guided Abstraction Refinement for Alternating Automata [ PDF ]
  • Alaska: Antichains for Logic, Automata and Symbolic Kripke structures Analysis [ PDF ]
  • Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking [ PDF ]
  • Provably Correct Code Generation of Real-Time Controllers (Master's thesis) [ PDF ]

    • Software

  • ALASKA uses antichains and ROBDD to solve the emptiness problem for finite and Buechi alternating automata. ALASKA also solves the LTL satisfiability problem and model checks LTL over NuSMV programs.

  • LaVaBDD  A simple C++ template library for Lattice-Valued BDD (online reference)

    • All versions of LaVaBDD:

    LaVaBDD-0.4   released on 20/04/2010 (online reference)
    LaVaBDD-0.3   released on 28/03/2010 (online reference)
    LaVaBDD-0.2   released on 26/02/2010 (online reference)
    LaVaBDD-0.1   released on 23/02/2010 (online reference)

  • SPECTRE is a tool that translates annotated Timed Automata into provably-correct C source code. More specifically, it generates real-time kernel modules for RTAI (a real-time Linux extension). The documentation for this tool is found in my Master thesis. SPECTRE is written in Haskell and can be compiled using the Glasgow Haskell Compiler and also requires the installation of Happy and Alex.