This repository was created as part of my research project at Mines de Nancy, supervised by Stephan Merz. The objective of the project is to mechanize a proof of correctness of a set-based algorithm inspired by Tarjan's algorithm for computing the strongly connected components of a graph. The algorithm is detailed in Vincent Bloemen's thesis and a few invariants are described.
In a similar way to "my thesis in 180s", I made a video briefly explaining my project, or more generally presenting the interest of formal methods in our current and future society. The video is available here.
The formal proof is written is Isabelle(HOL). I also wrote a LaTeX paper giving some details about the algorithm and its proof.
A TLA+ model for checking our invariants is provided in here.