6 citations · 10 across the 6 of their papers we have counts for
7 papers
Computer Aided Formal Design of Swarm Robotics Algorithms
Thibaut Balabonski, Pierre Courtieu, Robin Pelle +3
Previous works on formally studying mobile robotic swarms consider necessary and sufficient system hypotheses enabling to solve theoretical benchmark problems (geometric pattern fo…
Towards a Coq-verified Chain of Esterel Semantics
Gérard Berry, Lionel Rieg
This paper focuses on formally specifying and verifying the chain of formal semantics of the Esterel synchronous programming language using the Coq proof assistant. In particular,…
Dependent Pearl: Normalization by realizability
Pierre-Évariste Dagand, Lionel Rieg, Gabriel Scherer
For those of us who generally live in the world of syntax, semantic proof techniques such as reducibility, realizability or logical relations seem somewhat magical despite -- or pe…
Certified Universal Gathering in for Oblivious Mobile Robots
Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil +1
We present a unified formal framework for expressing mobile robots models, protocols, and proofs, and devise a protocol design/proof methodology dedicated to mobile robots that tak…
A Certified Universal Gathering Algorithm for Oblivious Mobile Robots
Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil +1
We present a new algorithm for the problem of universal gathering mobile oblivious robots (that is, starting from any initial configuration that is not bivalent, using any number o…
Impossibility of Gathering, a Certification
Pierre Courtieu, Lionel Rieg, Xavier Urbain +1
Recent advances in Distributed Computing highlight models and algorithms for autonomous swarms of mobile robots that self-organise and cooperate to solve global objectives. The ove…
Extracting Herbrand trees from Coq
Lionel Rieg
Software certification aims at proving the correctness of programs but in many cases, the use of external libraries allows only a conditional proof: it depends on the assumption th…