Your Mission

Gospel is a contract-based behavioural specification language for OCaml. It allows to give a logical model to OCaml types and describe the intended behaviour of a function using pre- and post-conditions.

QCheck-STM is a model-based testing framework for OCaml. Based on a description of the library API relatively to a system under test (for example a mutable data structure) and its functional model, it generates programs using the library API and runs them alongside the given functional model, keeping track of the correspondence between them at each step of the program.

Ortac/QCheck-STM is a fairly new tool that generates a QCheck-STM test suite based on the Gospel specification of a library. It is based on the Gospel logical model of the system under test. The intern should first get familiarised with Gospel, QCheck-STM and Ortac, possibly by writing specifications for a small library and extracting QCheck-STM tests using Ortac/QCheck-STM.

Then, the intern will be able to start working on adding features to Ortac/QCheck-STM. Among the possibilities, there are:

• include functions that don’t have a system under test as argument

• include functions that return a system under test

• include functions that have multiple system under test as arguments

• add support for libraries that don’t have an explicit system under test

(e.g., a file system library)

Your Key Responsibilities

• Understand Gospel specifications and be able to write specification for a simple library and extract some tests

• Understand how the QCheck-STM test framework works

• Work on extending Ortac/QCheck-STM test coverage, for example by

  • including functions that don’t have a system under test as argument

  • including functions that return a system under test

  • including functions that have multiple system under test as arguments

  • adding support for libraries that don’t have an explicit system under test (e.g., a file system library)

Your profile

• Functional programming
• Some knowledge of formal specification and verification
• Basic compiler knowledge

Why us?

• An opportunity to have an impact on a growing company and change the industry to use safer, more reliable, and more performant tools.

• Nice offices in the centre of Paris and Cambridge

• Flexibility to work remotely

• International team with 15 different nationalities

• Regular events with the whole team (Bi-yearly offsite, Monthly All-Hands meeting, monthly team-building event ...)

Our recruiting process' steps

If shortlisted, you will have two online interviews starting with a general interview with HR, followed by a technical discussion with the hiring manager.
We welcome applications from people of all backgrounds. We strive to create a representative, inclusive and friendly team, because we know that different experiences, perspectives and backgrounds make for a better workplace.