Tag Archives: Frama-C

not Taking Assumptions for Granted

The Merriam-Webster dictionnary defines an assumption as “a fact or statement (as a proposition, axiom, postulate, or notion) taken for granted”. This is indeed the role that assumptions play in formal verification of programs, as performed in Frama-C platform or GNATprove. Assumptions may either be related to the proof of a single function (like “this [...]

Posted in Certification | Also tagged , , | Leave a comment

A “Lighter” Introduction to Hi-Lite

The recently launched project Hi-Lite is based on powerful industrial tools that have been developed by the different partners for the last 10 to 25 years. This means in particular that it is not obvious to grasp the “vision” of Hi-Lite without knowing how all these tools work. To share this vision as broadly as [...]

Posted in Open-DO News | Also tagged , , , | Leave a comment
  • Categories

  • Open-DO Projects

  • Contact

    info @ open-do.org