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 [...]
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, [...]
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 [...]
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 [...]
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) + [...]
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 [...]
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 [...]
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 [...]