Chargement Évènements

« Tous les Évènements

  • Cet évènement est passé

Séminaire Méthodes Formelles

février 20 @ 15:00 - 16:00

FM seminar by Arthur Charguéraud (Inria & ICube, Université de Strasbourg)

Date: Tuesday, February 20th
Time: 15h00
Room: A008

Verification of Imperative Programs using CFML

Abstract :
CFML is an interactive tool that supports modular verification of higher-order, imperative programs. It is entirely implemented inside the Coq proof assistant. CFML leverages two key ingredients. First, it relies on an embedding in Separation Logic to describe the mutable state. Second, it relies on the construction of Characteristic Formulae for smoothly integrating the process of verifying in Coq the code line by line. CFML has been applied to verify classical data structures and algorithms, including binary search trees, hashtables, finger trees, catenable and splittable chunk sequences, Dijkstra’s shortest path algorithm, depth first search, vectors, Eratosthenes’ sieve, and Union-Find. Furthermore, CFML has been recently extended to support amortized complexity analysis. In this talk, I will give a tour of CFML, covering both its implementation and its use in practice. Experience with Coq is not required to follow the talk.

Share on FacebookShare on Google+Tweet about this on TwitterShare on LinkedIn


Date :
février 20
Heure :
15:00 - 16:00
Catégorie d’Évènement:

En ce moment

Colloquium Loria 2018

Exposés précédents

Logo du CNRS
Logo Inria
Logo Université de Lorraine