Loïc Germerie Guizouarn

I'm PhD student in computer science in I3S lab, part of Université Côte d'Azur (in Sophia Antipolis, near Nice), under the supervision of Étienne Lozes and Cinzia Di Giusto. My main research interests are formal verification and specification of communication protocols.


PhD Subject

Most of the distributed systems we use nowadays are based on the message-passing paradigm where systems are structured into parties that interact only by sending and receiving messages. Message-passing programming is largely employed in high performance computing (MPI, OpenMP, etc), event-driven applications built on top of actor-based languages (Scala, Erlang, etc), service-oriented architectures, peer-to- peer applications, etc.

Unfortunately, because of the variety of communication models (peer to peer, mailbox, etc.), of the ambiguities of the specifications of the communication primitives, of a limited portability of the code, and of the difficulty of running representative tests, etc., it is error prone and therefore often reserved to experts.

Model-checking of communicating machines aims at analysing formal models of distributed systems and discovering bugs like message loss or deadlocks. This problem is undecidable in general, even with two machines only, and several restrictions have been considered to restore decidability. One of them is the hale-duplex hypothesis: in a system of two machines, it is always the case that a machines does not send any message if it still has some pending messages to be received in its queue.

The goal of this phD thesis is to define new classes of communicating machines for which model-checking is decidable, among other by extending the notion of half-duplex systems to systems of arbitrary number of machines. Possibly, this would involve to introduce a separation logic for communicating machines that captures these generalised half-duplex properties.


  • Towards generalised half-duplex systems
    Cinzia Di Giusto, Loïc Germerie Guizouarn, and Etienne Lozes
    ICE 2021, Online, 18th June 2021, volume 347 of EPTCS, pages 22–37, 2021.
  • Formalising Futures and Promises in Viper
    Cinzia Di Giusto, Loïc Germerie Guizouarn, Ludovic Henrio, and Étienne Lozes
    33èmes Journées Francophones des Langages Applicatifs, June 2022


I taught in the second year of the computer science degree. I taught Mechanisms of Operating Systems and C language programming and datastructures.

Contact information

  • Address

    Office 222
    Laboratoire I3S - UMR CNRS 7271
    2000, route des Lucioles
    06900 Sophia Antipolis