Verification of Asynchronous Communication

This demonstrator was developped in 2015-2016 during Florent Chevrou's PhD and Nathanaël Sensfelder's master thesis, under the supervision of Aurélie Hurault and Philippe Quéinnec.
The verification framework has been developped by Florent Chevrou, Nathanaël Sensfelder and Philippe Quéinnec. The web site has been developped by Nathanaël Sensfelder.

Related Publications

• Automated Verification of Asynchronous Communicating Systems with TLA+, Florent Chevrou, Aurélie Hurault, Philippe Quéinnec.
  In Electronic Communications of the EASST, Special issue Proceedings of the 15th International Workshop on Automated Verification of Critical Systems, Vol. 72, 2015.
• On the Diversity of Asynchronous Communication, Florent Chevrou, Aurélie Hurault, Philippe Quéinnec.
  Formal Aspects of Computing, Springer, to appear in 2016.
• Mechanized Refinement of Communication Models with TLA+, Florent Chevrou, Aurélie Hurault, Philippe Quéinnec.
  ABZ 2016, LNCS 9675, 312-318, 2016.
• Inference of Channel Priorities for Asynchronous Communication, Nathanaël Sensfelder, Aurélie Hurault, Philippe Quéinnec.
  14th International Conference on Distributed Computing and Artificial Intelligence (DCAI'17), june 2017.
  extended version.

Aurélie Hurault

Personal web page

Florent Chevrou

Nathanaël Sensfelder

Personal web page

Philippe Quéinnec

Personal web page