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 challenging and time constrained, nonetheless OCamlPro met the requirements in time while producing a code of excellent quality.”
David Mentré, MERCE
Months and months of lockdown have allowed us to take the time to look back on events of the past years and to advertise our strong ties with academic and industrial partners, and our achievements through an exhaustive Timeline of OCamlPro’s story of which you can find a small excerpt below.