Software Verification / Vérification de logiciel

Entries feed - Comments feed

Last entries

Thu 21 Nov 2013

  • David Mentré
  • 1

Introduction aux méthodes formelles actualisée

Comme en 2010 et 2011, j'ai faire une intervention de 2h pour présenter les méthodes formelles à l'ESIR, école d'ingénieur de Rennes 1. J'ai un peu actualisé la présentation, je pense qu'elle est plus illustrée et j'ai introduit quelques démonstrations d'utilisation des outils. La présentation est disponible en PDF ou en source au format PowerPoint (licence Art Libre, sauf pour les illustrations, que j'ai pioché à droite et à gauche sur le web).

Note pour les libristes : la plupart des logiciels mentionnées sont libres.

Fri 04 Oct 2013

  • David Mentré
  • 2

Introductory slides on Frama-C

I recently made at work slides to present Frama-C: what it is, the various plug-ins and how to use the two main ones, Value analysis and WP. The examples used in the slides are also available.

The attached version is updated after fixing minor issues found by frama-c-discuss mailing list readers.

Enjoy! (and let me know if you find them useful)

Mon 17 Dec 2012

  • David Mentré
  • 3

How to install Atelier B 4.1 on a Debian-like 64 bits machine

Atelier B 4.1 has just been released. For Linux machines, it is available as a binary packages for 32 bits x86 machines in RPM and DEB format. Unfortunately the DEB package won't work on a Debian-like 64 bits machine, for example an Ubuntu. Here the approach have I used to install the package:

Install Atelier B 4.1 in /opt/atelierb-4.1

  • mkdir /tmp/ab
  • cd /tmp/ab
  • wget
  • ar xv AtelierB-4.1.0-free-linux.deb
  • cd /
  • sudo tar zxf /tmp/ab/data.tar.gz
  • sudo chown -R YourUserID:YourGroup /opt/atelierb-4.1/ # substitute YourUserID and YourGroup with adequate values

Configure the execution environment on an Ubuntu 12.04

  • sudo apt-get install ia32-libs-multiarch

You can now start Atelier B with:

 /opt/atelierb-4.1/startAB &

The procedure might be different for another Debian-like distribution, including Debian itself. You can add specific procedures for a given distribution in the comments.

Sat 21 Jul 2012

  • David Mentré

Which approach for Hoare logic formal verification?

Currently, if one wants to do some program verification using Hoare logic framework, three approaches are possible:

  1. Down to code approach, when one annotates code functions with pre and post-conditions. This is the approach proposed by Frama-C on C code, SPARK on Ada code or GNATprove on Ada code. This approach has the advantage to be directly palatable to programmers because they are keeping they preferred language. Moreover, one can use such approaches on existing code, even if to fully verify it one will probably need to make some change. The downside of the approach is that the formal verification is tightly linked to the code, making the formalisation of program wide properties more complex;
  2. Abstract specification refined in implementable code, like the B Method (and its variant Event B for system specification). This approach using using pre and post-conditions but also invariants on which all the correctness of the code is built. Due to its abstract specification, it can express complex properties that help reasoning on the built program or system. However, it uses very mathematical concepts like set theory or relations which are making engineers not at ease. And the proof can be somewhat complex, involving some manual steps. Moreover, one needs to fit its development process in B approach, without reuse of existing code;
  3. A new approach proposed by Bertrand Meyer (of Eiffel fame which popularized the Design by Contract approach) which relies on pre and post-conditions on code but where such specification can use more abstract operators made available from libraries called Domain theories. The main idea is that such domain theories provide to the programmer abstract view on some domains (like maximum of an array) so formal specifications are easier to read (and thus probably more correct) and hopefully to prove.

The third approach of Meyer seems to take most advantages of the two first ones: use of current programming language so the programmer is at ease and use of abstract formalisation so the specification is easier to read and more abstract. Moreover, it relies heavily on invariants (already available in Eiffel language) so a B Method-like approach is possible. However, Meyer's approach lacks refinement capabilities of B Method. But as far as I know, refinements are rarely used in B Method, except for making difficult proofs easier by using several steps to make concrete algorithms or data structures[1].

It remains to see how it will be implemented in a tool. Formal methods effective capabilities are determined by the supporting tools. Time will tell if Meyer's approach is really useful! :-)


[1] But that might make the difference between a nice approach and a usable one. ;-)

Fri 29 Jun 2012

  • David Mentré

An nice tutorial on basic logic

I have recently seen in Lambda the Ultimate an announcement for an interactive tutorial on first order logic. It is really nice to visually see the application of the logic rules, as well as proving things (aka get the proof obligation get green) just by clicking.

With such an interface, proof is like a game! :-)

Thu 07 Jun 2012

  • David Mentré
  • 4

A proved toy electronic voting booth program in Ada

Three years ago, in March 2009, I wrote a toy electronic voting booth program in C language. The goal was to formally verify it using the Frama-C/Jessie framework. The program was short enough to be entirely understood in a short time but complex enough (with arrays, integer arithmetic, strings, I/O, ...) to exert formal verification techniques.

Since then, Hi-Lite project has started, with the aim of providing tools to mix formal verification and tests in the same program, following Design-by-Contract approach. Hi-Lite tools are supporting two languages, C extended with ACSL, Frama-C's specification language, and Ada 2012 that now supports Pre-conditions and Post-conditions on procedures.

Thus I attempted to do a similar work using AdaCore's GNATprove verification tool. The result is now publicly available as ada-evoting-0.2, under a very liberal BSD license, thanks to the help of Claire Dross and Yannick Moy of AdaCore. They helped me write the last invariants and fix the last bugs. All the Verification Conditions (VC) can now be automatically proved using Alt-Ergo, an SMT solver available as free software and developed by ProVal research team of INRIA/LRI.

The program has been verified with latest release of GNATprove. GNATprove is not yet publicly available but Yannick announced that a GPL release of it should occur before the end of this month. So, in a short time frame one should have all needed free software (IDE, compiler, VC generator and automatic prover) to write and prove Ada programs, with a small example of its use. Nice isn't it? :-)

There still a lot of things to do on that small program, like using GNATtest to test it in the usual way or make a SPARK version to formally verify it with SPARK tools (of which a new GPL edition should be release shortly). But, as usual, days are not long enough. ;-)

PS: Ada is very nice to write such kind of low level software. I haven't used it for more than 10 years but I really enjoyed using again the language.

Mon 12 Mar 2012

  • David Mentré
  • 11

New paper accepted on use of Why3 as another proof toolchain for Atelier B

In 2011, in collaboration with Jean-Christophe Filliâtre and Claude Marché of ProVal team at INRIA/LRI and Masashi Asuka of my company, we have plugged Why3 proof tool-chain into Atelier B. More exactly, we wrote a tool called bpo2why and associated Why3 theories to transform Proof Obligations generated by Atelier B into Why3 verification conditions. Those verification conditions can then be checked with several automatic provers (we have used Alt-Ergo, CVC3 and Z3). Overall, we are quite satisfied with the result, the automatic provers of Why3 proof tool-chain proving more proof obligations that native Atelier B automatic prover (F0 and F1). We made an article about this work and this article has been accepted at ABZ 2012 conference! :-)

For further details, just read "Discharging Proof Obligations from Atelier B using Multiple Automated Provers" (PDF).

Sun 15 Jan 2012

  • David Mentré
  • 1

Présentation de l'analyse statique avec Frama-C

Comme l'année dernière, j'ai fait une présentation à des étudiants ESIR 2 (école d'ingénieur de la Fac de Rennes 1) de l'analyse statique avec l'outil Frama-C et son analyse de valeur. Les sources (format propriétaire, licence Art Libre) et le PDF des transparents sont disponibles, ainsi que les exemples.

Thu 08 Dec 2011

  • David Mentré
  • 2

Introduction aux méthodes formelles

Comme l'année dernière, j'ai fait une introduction aux méthodes formelles aux étudiants d'ESIR 3, l'école d'ingénieur de l'université de Rennes 1 (anciennement DIIC).

Et comme l'année dernière les transparents sont disponibles, au format PDF ou les sources au format propriétaire PPTX (LibreOffice peut ouvrir le fichier). Ils sont libres, sous licence Art Libre 1.3, sauf pour quelques images, récupérées sur le web et propriété de leurs auteurs.

Promis, l'année prochaine je ferai ma présentation (ou une nouvelle présentation sur le même thème) uniquement avec des outils Libres ! ;-)

Tue 01 Feb 2011

  • David Mentré

Frama-C pour l'analyse de valeur et la preuve

J'ai fait hier soir une présentation Gulliver sur Frama-C, un framework qui permet notamment de faire de l'analyse et de la preuve sur du code C. Les transparents et exemples sont disponibles (réutilisez les, c'est du Libre !).

Suite à l'annonce de ces transparents sur la liste frama-c-discuss, une très intéressante discussion a démarré sur l'utilisation concrète de Frama-C sur des codes industriels et les avantages respectifs de l'analyse de valeur et la preuve. Je recommande de lire notamment les points de vue de quelqu'un d'Atos Origin (avec des remarques encore plus précises sur la manière de faire ces analyses) et de quelqu'un de chez Dassault Aviation.

Apparemment, Frama-C est utilisé sur du code industriel et il donne des résultats. Intéressant !

page 1 / 2