Topic of my Ph. D. thesis

The Focal correct-by-construction environment is developed by the Focal project (initiated by T. Hardin and R. Rioboo and further developed by researchers coming from LIP6, CÉDRIC and INRIA), allows one to incrementally build library components with a high level of confidence and quality. A component of a Focal library can contain specifications, implementations of operations and proofs that the implementations satisfy their specifications. Focal components are translated into OCaml executable code and are verified by the Coq proof assistant.

My thesis deals with the design and development of a testing tools to be integrated into Focal. Focaltest is a testing-tools inspired from QuickCheck and permits to test properties automatically with a test-and-generate approach for test data selection through the usage of constraint reasoning. It consists in exploring very carefully the precondition part of the property under test and more precisely the definition of the implementation, upon which the precondition holds, in order to produce constraints over the quantified variables.