206
9 March 2017 - 15h30
Formal Proofs of Safety in Coq: Mobile Robot Networks and Lustre Compilation
by Lionel Rieg from Yale university, Flint group
Abstract: In the first part, I will look into the verified compilation of the synchronous language Lustre. The objective of this work is to build a proven compiler from Lustre to C and connect it to CompCert, a proven compiler from C to assembly, to have a fully verified compilation chain toward assembly code. Although the compiler is straightforward to write, the difficulties are in the proof of correctness of the compilation scheme and they are very different from the ones of CompCert as they stem from the disparity of semantic models: to go from a synchronous language to an imperative one.
In the second part, I will present the Pactole project which builds a formal framework in Coq to reason about mobile robot networks. This framework is flexible enough to encompass the variations of the model by changing parameters (number of byzantine faults, perception capabilities of the robots, synchronization hypotheses, ...). I will illustrate this framework on a fundamental problem, the gathering, which aims at having all robots reach the same location (unknown beforehand) in finite time. In all generality, this problem is unsolvable, with a formal proof in Pactole to witness it. Nevertheless, I will give an algorithm that is correct except for one unique starting position, exactly the one used to prove the impossibility in the general case.
