Author Archives: Yannick Moy

ERTS 2014: Integrated and Simpler Systems

I attended last week the 7th edition of the congress on Embedded Real Time Software and Systems that takes place in Toulouse (France) every two years. It started with Joseph Sifakis inviting all of us to work on the integration of embedded systems with Internet, and the Engineering Executive Vice-President of Airbus, Charles Champion, describing [...]

Posted in Certification, Events | Leave a comment

Using Formal Verification in the Landing Field

An article which I co-authored was just published in the May-June special issue of IEEE Software on Safety-Critical Software. It’s called Testing or Formal Verification: DO-178C Alternatives and Industrial Experience, and it talks about how to use formal verification instead of testing for software in civilian airplanes (for which DO-178C applies). It is based on [...]

Posted in Papers and Slides | Tagged , | 3 Comments

GNATprove Takes the Train

David Mentré from Mitsubishi Electric R&D Centre Europe has produced a very interesting report on his use of GNATprove (the formal verification tool we develop for the next version of SPARK) on a case-study from the Open-ETCS European project, to develop the tools for the future European Train Control Systems.

Although David asked me to [...]

Posted in Open-DO News | Tagged , , | 5 Comments

Axioms and Proofs: When Less is More

In formal verification, we ultimately rely on automatic provers to decide whether formulas are valid (always true) or not. In GNATprove for example, we rely mostly on the ability of prover Alt-Ergo to analyze quickly the formulas we generate, and answer yes when the formula is valid or no when the formula is invalid (so [...]

Posted in Open Source | Tagged , , | Leave a comment

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 | Tagged , , , | Leave a comment

Future Version of SPARK Will Be Based on Ada 2012

At the SPARK User Day yesterday in Bath, Altran-Praxis and AdaCore announced that the SPARK language will undergo a major transformation, to both extend the subset of Ada included in SPARK, and to use the new specification features of Ada 2012 instead of special comments like in today’s SPARK language. This is only fair that, [...]

Posted in Events, Open Source | Tagged , , | Leave a comment

GNATprove Distinguished at VerifyThis Competition

I participated last week in the VerifyThis Verification Competition, which took place on Thursday afternoon during the Formal Methods 2012 conference in Paris. The goal was to apply verification tools to three small challenge programs, to compare approaches and learn from each other’s tools.

I used Ada 2012 as a programming and specification language (using preconditions [...]

Posted in Events | Tagged , , , , | 1 Comment

ESA is Funding Students on Open-Source Projects this Summer

The European Space Agency is reediting its SOCIS initiative this year. Open-source projects can submit proposals, and ESA will fund between 20 and 25 students to work during two months on these projects.

We submitted a project to extend our work on standard containers adapted to formal verification. Submit yours by July 15th!

Posted in Open Source, Related Initiatives | Leave a comment

Certification, Safety and Security at ERTS 2012

We are now leaving the Embedded Real Time Systems and Software conference which was held in Toulouse for the last 3 days. The conference has been expanding since the last occurrence in 2010, with more international presence, many German companies in particular, and a large number of companies from the automotive industry (maybe this is [...]

Posted in Events | Tagged | Leave a comment

Prove Your Plane Now!

The DO-333 is now available! (ok, that’s not free: 215$ for an electronic version, or 300$ for a hard copy, pfew!)

Under this amazingly explicit name is hiding the formal methods supplement for DO-178C. Or, said otherwise, the document that allows you, as a developer of avionics software, to replace tests/reviews/analyses by formal methods. Or you, [...]

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

  • Open-DO Projects

  • Contact

    info @