Tag Archives: Hi-Lite

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 | Also tagged | 1 Comment

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 | Also tagged , | 2 Comments

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

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 | Also 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 | Also tagged , , , | 1 Comment

Integrating Formal Program Verification with Testing

This is the paper that Yannick Moy presented at the recent ERTS 2012 conference:
Verification activities mandated for critical software are essential to achieve the required level of confidence expected in life-critical or business-critical software. They are becoming increasingly costly as, over time, they require the development and maintenance of a large body of functional and [...]

Posted in Certification, Events, Open Source, Open-DO News, Papers and Slides | Also tagged , , , | Leave a comment

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 | Also 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 | Also 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 | Also tagged , | 1 Comment

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 | Also tagged | Leave a comment
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @ open-do.org