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