Automated runtime assertion checking for OCaml

Mentor: Clément Pascutto

Location: Tarides office, Paris

Runtime assertion checking (RTAC) is the discipline of detecting runtime violations of program properties and invariants. Those properties are usually expressed as function contracts in a high-level specification language. Unlike formal verification with proof assistants, that usually require more effort and expertise, runtime assertion checking aims at simplicity of use and accessibility for programmers, allowing them to formally specifying their programs without the hassle of formal proofs.

This approach has been successfully implemented to dynamically verify various mainstream languages; E-ACSL is a specification language and RTAC tool part of Frama-C that aims at checking C programs, jmlrac is a runtime assertion checker for Java's JML specification language. However, there is no such tool for the OCaml ecosystem yet.

The goal of this internship is to contribute to the development of a runtime assertion checking tool for the OCaml ecosystem, developed at Tarides. It is based on the Gospel specification language for OCaml, which enables the programmers to provide formal contracts for the functions exposed by their libraries:

(*@ open Seq     *)
(*@ open SeqPerm *)

(*@ predicate k_values (k: int) (a: int seq) =
      forall i: integer. 0 <= i < length a -> 0 <= a[i] < k *)
val counting_sort: int -> int array -> int array -> unit
(*@ counting_sort k a b
      requires 0 < k
      requires k_values k a
      requires length a = length b
      modifies b
      ensures  Seq.sorted b
      ensures  SeqPerm.permut_all a b *)

Those contracts are then automatically translated to instrumented implementations that check their correctness at runtime without altering its semantics if they comply to the specification.

The goal of this internship is to apply those methods to:

  • Formally specify existing libraries that are heavily used in the Mirage/Irmin ecosystem, and test them.
  • Contribute to the development of the tool by adding support for more constructs and improving its integration with the existing ecosystem.

This internship will be held as part of a close collaboration between Tarides and the VALS team of the LRI laboratory.

Necessary skills

  • Non-trivial functional programming experience
  • Ability to read scientific publications and implement concepts described in them
  • Familiarity with formal specification/verification is useful, but not required