Author Archives: Yannick Moy

Executable Annotations for C Programs

The Frama-C platform, which integrates static analysis and formal proof of C programs, now has a plug-in for run-time execution of annotations. In particular, preconditions and postconditions written using the E-ACSL subset of the ACSL annotation language for C can now be executed thanks to this plug-in. This is a great move in the direction [...]

Posted in Open-DO News, Related Initiatives | Tagged , | Leave a comment

Prove & Fly!

On December 5-6, I participated in the 2nd workshop on Theorem Proving in
Certification, in Cambridge (UK). This turned out to be even more interesting than last year’s program promised.

The goal of the workshop is to clarify under which conditions theorem proving
can be applied in the context of DO-178C Formal Methods Supplement (hence Prove & Fly!):

extent [...]

Posted in Certification, Events | Tagged , , | Leave a comment

Cookbook for Applying Formal Methods in Industry

If you read a bit of French, you’ll be happy to know that Hermes Publishing has just issued the first of a three-volume series on
Utilisations industrielles des techniques formelles (use of formal methods in industry). This first volume is concerned with abstract interpretation techniques and tools.
As such, we at AdaCore contributed a chapter on [...]

Posted in In the Press | Tagged , , | 1 Comment

Best Paper Award for Results of Verification Competition

Last year, the conference VSTTE 2010 organized a competition of software verification systems (language + tools),
to improve understanding of each system’s pros and cons. Rod Chapman from Altran Praxis participated with the SPARK language
and toolset, and solved the first problem even beyond what the subject asked. We have since provided solutions in SPARK to all [...]

Posted in Certification, Events, Papers and Slides | 1 Comment

Language Vulnerabilities for Dummies

In case you do not know the series of books “for Dummies”, its principle is
to explore a subject from the ground up, with rich explanations and examples
for non-experts. That’s in my view a valid alternative title for the recently
published “Guidance to Avoiding Vulnerabilities in Programming Languages
through Language Selection and Use”. Rich (around
70 vulnerabilities explored) + [...]

Posted in Certification, Papers and Slides | 6 Comments

Being Elmer Fudd

Ever found yourself in an extreme stressed state because of some bugs* escaping you? Then you know how it feels to be Elmer Fudd. Not a typical hero, never victorious in his hunt. So it feels being a software engineer. A new episode in this tragicomedy is a paper by Yang et al. from Uni [...]

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

Proving Alt-Ergo prover in Coq

I attended yesterday the PhD defense of Stéphane Lescuyer, who presented his work on the proof of prover Alt-Ergo, pushing the boundary of what’s feasible with today’s proof technology.

First, a few words of why this is interesting for us at AdaCore, in an industrial setting. Starting with SPARK Pro 9.1, users now have the [...]

Posted in Certification, Events | Tagged , | 5 Comments

Case Study: Can you afford to ignore formal analysis?

This is a title I’d like to reuse some day for a case study in Hi-Lite, but right now it is the title of a very interesting paper published by EE Times: people from Alcatel-Lucent formally verified many properties of an ASIC design in a large communication system.

What is stricking is the similarity of the [...]

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

Hi-Lite Progress: Discussions on Specification Languages

We had yesterday our first joint meeting in Hi-Lite since the start of the project, 6 months ago. This was the occasion for CEA to present their ideas for E-ACSL (the executable fragment of the ACSL specification language for C) and for us at AdaCore to present our ideas for ALFA (the subset of Ada [...]

Posted in Open-DO News | Leave a comment

DO-178C Expected for Q1 2011

According to this article, which gives an overview of the changes introduced by this new version of the avionics standard.

I like her presentation of Formal Methods:

Formal methods are a class of mathematically based techniques used for the specification, development, and verification of avionics software. Formal methods tools, for example, are used to represent an aircraft’s [...]

Posted in Certification, In the Press | 2 Comments
  • Categories

  • Open-DO Projects

  • Contact

    info @