Tag Archives: Formal verification

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 | 3 Comments

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 , | 5 Comments

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

ImProving Formal Verification

We learned this week of ImProve, a lightweight DSL intended for building high assurance embedded applications. Developed by Tom Hawkins, the tool is an EDSL that performs formal verification (via. model checking) and code generation. The host language is Haskell; meaning ImProve programs are nothing more than Haskell programs that call the ImProve library [...]

Posted in Agile/Lean Programming, Certification | Also tagged | Leave a comment

Case Study: Can you afford to ignore formal analysis?

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

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

Must-see Videos on Code Verification

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

Posted in Videos | Also tagged | Leave a comment
  • Categories

  • Open-DO Projects

  • Contact

    info @ open-do.org