Author Archives: Yannick Moy

Use of Formal Methods in Avionics Triggers Interest in Railway

I was invited today to give a talk at Fraunhofer FIRST, a German research institute, on Formal Verification in Aeronautics: Current Practice and Upcoming Standard. I told them about the pioneering work done at Airbus, especially related to unit proof to replace unit testing, and about the new version of the DO-178 standard (the ‘C’ [...]

Posted in Certification, Events | 2 Comments

Must-see Videos on Code Verification

Rustan Leino, a researcher at Microsoft Research, has started creating a set of videos where he both teaches and demoes how to do code verification with the tools developed at Microsoft Research. This shows how to overcome the difficulties than someone may encounter with every code verification tool, except the GUI is amazingly intuitive (verification [...]

Posted in Videos | Tagged , | Leave a comment

Embedded Contract Languages by Microsoft Research

People from the group developing Spec# at Microsoft Research finally published an article on their new Code Contracts approach.

Chosen excerpts: “embedding of contracts as code is a better approach”; “The language of conditions is just the language of expressions
in the programming language used”; “ForAll and Exists that work over integer ranges and collections”; “Any methods [...]

Posted in Open-DO News, Papers and Slides | Tagged , | Leave a comment

ERTS² conference week

I spent a very interesting week in Toulouse last week. It started with a day of conference in which INRIA research labs showed a host of products and advanced research applicable to the domains of modeling and safety. There was in particular demos of Astrée (static analyzer for C, now sold by AbsInt Gmbh), Frama-C [...]

Posted in Certification, Events, Open-DO News | 1 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 | Tagged , , , , | Leave a comment

David Crocker’s Verification Blog

In case you missed the very interesting blog that David Crocker of Escher Technologies is writing since January of this year, I have put a link to it in the Blogroll that you find on the right of the Open-DO main page. David’s ArC system reads C code together with annotations written in special macros [...]

Posted in Open-DO News | Leave a comment

AdaCore Awarded Grant for Hi-Lite Project

Earlier this month, on March 3rd, AdaCore was awarded a grant by the French government and local
authorities to develop an innovative set of tools integrated with its GNAT Pro
platform. AdaCore is leading a consortium of 2 research institutes (CEA-List,
the ProVal team of INRIA) and 4 industrial companies (AdaCore, Altran, Astrium
and Thales Communications) in this [...]

Posted in Open-DO News | Leave a comment

Formal Methods Week 2009

Last month I attended part of the Formal Methods Week 2009 in Eindhoven. Each year the FMWeek brings the world of formal verification together, with an emphasis on academic and industrial partnerships.

Although I am familiar with the field, I was still impressed by what is currently possible with tools based on formal methods. Although [...]

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

  • Open-DO Projects

  • Contact

    info @