May 2023 - July 2023: Research Intern
Formal Methods Laboratory (LMF) Orsay, Toccata Team, Inria
Location: Orsay, France
Supervisors: Jean-Christophe Filliâtre and Andrei Paskevich
Project: Why3 Transformations and Binary Decision Diagrams
This internship had two main aspects focusing on the Why3 platform and formal verification techniques:
- Developed a verified library of binary decision diagrams (BDDs) in Why3 (~220 lines of code and ~220 lines of specifications). This library constructs optimised BDDs with guaranteed optimal complexity in terms of time and memory thanks to hash-consing (maximum sharing).
- Created a logical transformation system for breaking down complex proof goals into easier-to-prove subgoals.
Technologies: Why3, BDD, Formal Proofs, OCaml
Repositories:
Links: Internship Report | Project Code | Why3 Session Summary