Tag Archives: formal methods

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

Use of formal methods in critical systems conference

This conference will take place in Toulouse on November the 12th. It is in French as is the announcement providing more details below:

Les animateurs du DAS Systèmes Embarqués, avec le soutien du thème IFSE du RTRA AE/SE, ont le plaisir de vous annoncer la programmation d’un cycle de conférences techniques sur les méthodes formelles de [...]

Posted in Certification, Events | Also tagged , | Leave a 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

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

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

  • Contact

    info @ open-do.org