Tag - paper

Entries feed - Comments feed

Last entries

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).

New paper accepted on B Method and Model checking

I proposed a paper to ITST 2010 conference and it has been accepted!

The core proposal of this paper is to link low level B Method model (B0 code) to Model checking techniques. More exactly, I propose to automatically extract a SPIN model in Promela language from a B0 model. I applied this approach on a simple model of a railway level crossing.

For further details, just read "Checking temporal properties on state based formal specification: application to railway level crossing"! ;-)