Ph.D. project: Runtime Verification of OCaml Programs
I started working on my Ph.D. project in 2020 under the supervision of Jean-Christophe Filliâtre in the Formal Methods Laboratory (LMF) of the Paris-Saclay University. It is funded and supported by Tarides.
I am interested in making formal methods more accessible and practical to developers. My work aims at providing a tool and workflow to automatically test formal specifications attached to OCaml interfaces. It is a good middle ground between formal verification and vanilla handwritten tests.
I contributed to several open-source projects:
- Gospel, a specification language for OCaml.
- Ortac, a runtime assertion checker for Gospel and OCaml.
You may also read articles published about my work:
- Ortac: Runtime Assertion Checking for OCaml. An introduction to the Ortac runtime assertion checker as I started developing it: its main features, design choices, and limitations.
- Optimizing Prestate Copies in Runtime Verification of Function Postconditions. An article on producing more efficient (and correct!) verifications for postconditions that refer to the prestate memory.
- Leveraging Formal Specifications to Generate Fuzzing Suites. A presentation showing how we can combine Ortac’s runtime verification with fuzzing techniques to generate fully automated test suites from specifications. A joint work with Nicolas Osborne.
Dissertation
The final version of my dissertation is available here.
Abstract
Formal verification methods, in particular when it comes to deductive verification, bring strong guarantees about the correctness of software systems. However, they require a high degree of expertise and tremendous development time. These pitfalls sometimes jeopardize their application in industrial-grade software, almost always preventing scaling to complex systems. In that respect, dynamic (read: runtime) verification allows for a more gradual approach. While the user still expresses specifications in a formal, precise language, one checks the correctness of the implementation *via* automatic testing at runtime rather than proofs. It narrows the required expertise to the specification design and the interpretation of test results.These observations also apply to the OCaml programming language community. Despite the suitability of the language for formal methods, broad adoption still seems out of reach for tools that produce specified or verified code. Moreover, such tools must account for details of the language: its type system, memory representation, garbage collector, and functional idioms.
In this work, we propose runtime verification techniques for OCaml code that apply to preexisting codebases and engineers’ workflows. In particular, we briefly introduce Gospel, an accessible yet expressive specification language for OCaml. We describe Ortac, an automated runtime assertion checker for OCaml with a modular interface that allows for multiple usage scenarii (fuzzing, monitoring, tests). Ortac aims to support a non-trivial subset of OCaml (e.g. functors, exceptions, effects). It uses typing information to produce efficient verifications (e.g. narrowing the copies, handling arbitrary precision integers, partially verifying type invariants). Lastly, we elaborate on memory optimizations for verifying postconditions referencing the prestate. They consist of specification transformations, generalized to apply to other languages, that have been proven correct using the Coq proof assistant.
This work opens a way for an automated verification ecosystem that would be unintrusive and suitable for the developers’ needs in the OCaml community.
Defense
I publicly defended my Ph.D. dissertation on October 18, 2023, at 2PM, in the Paris-Saclay University.