FM seminar by Arthur Charguéraud (Inria & ICube, Université de Strasbourg)
Date: Tuesday, February 20th
Verification of Imperative Programs using CFML
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.