Project with MERCE (Mitsubishi Electric R&D Centre Europe) in Rennes, France
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 involved and time constrained, nonetheless OCamlPro met the requirements in time while producing a code of excellent quality.”