Internship: Formal verification of Fortune's algorithm

Formal verification of Fortune's algorithm

Fortune's algorithm is a sweep line algorithm to construct the Voronoi diagram of a set of points in the plane. Voronoi diagrams have applications in many domains of activities, for instance concerning antenna placement and robot motion planning. In this task, we wish to develop a formal description of Voronoi diagrams and of the algorithm proposed by Steven Fortune in 1986, in the context of the Coq system and the mathematical components library. If time allows, we also wish to study how executable algorithms can be derived from the formal description.

The intern will have to work with the Coq system. Documentation for the various aspects of the work can be obtained in the following manner:

This internship will be supervised by Yves Bertot, senior research scientist at Inria.