Project with MERCE (Mitsubishi Electric R&D Centre Europe) in Rennes, France (June 2019)
Starting from a specification provided by MERCE, we designed and implemented a formal verification analysis tool to check a particular class of safety properties over C programs. The tool was implemented as a Frama-C plug-in and came with fully fledged user and formal documentation.
“MERCE was very satisfied of OCamlPro. The project was technically demanding and time constrained, nonetheless OCamlPro met the requirements in time while producing a code of excellent quality.”