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 [...]
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 [...]
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’ [...]
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 [...]
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 [...]
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 [...]
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 [...]
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 [...]
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 [...]