Wiki Agenda Contact Version française

Publications : Fran├žois Bobot

Back
[20] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.86.1. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.86.1 edition, May 2015. http://why3.lri.fr/download/manual-0.86.1.pdf. [ bib | full text on HAL | .pdf ]
[19] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Let's verify this with Why3. International Journal on Software Tools for Technology Transfer (STTT), 17(6):709--727, 2015. See also http://toccata.lri.fr/gallery/fm2012comp.en.html. [ bib | DOI | full text on HAL ]
[18] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.82. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.82 edition, December 2013. http://why3.lri.fr/download/manual-0.82.pdf. [ bib | full text on HAL | .pdf ]
[17] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. Preserving user proofs across specification changes. In Ernie Cohen and Andrey Rybalchenko, editors, Verified Software: Theories, Tools, Experiments (5th International Conference VSTTE), volume 8164 of Lecture Notes in Computer Science, pages 191--201, Atherton, USA, May 2013. Springer. [ bib | full text on HAL ]
Keywords: Why3
[16] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.81. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.81 edition, March 2013. http://why3.lri.fr/download/manual-0.81.pdf. [ bib | full text on HAL | .pdf ]
Keywords: Why3
[15] François Bobot and Jean-Christophe Filliâtre. Separation predicates: a taste of separation logic in first-order logic. In 14th International Conference on Formal Ingineering Methods (ICFEM), volume 7635 of Lecture Notes in Computer Science, Kyoto, Japan, November 2012. Springer. [ bib | full text on HAL | .pdf ]
This paper introduces separation predicates, a technique to reuse some ideas from separation logic in the framework of program verification using a traditional first-order logic. The purpose is to benefit from existing specification languages, verification condition generators, and automated theorem provers. Separation predicates are automatically derived from user-defined inductive predicates. We illustrate this idea on a non-trivial case study, namely the composite pattern, which is specified in C/ACSL and verified in a fully automatic way using SMT solvers Alt-Ergo, CVC3, and Z3.

[14] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.80. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.80 edition, October 2012. https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf. [ bib | .pdf ]
Keywords: Why3
[13] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.73. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.73 edition, July 2012. [ bib | .pdf ]
Keywords: Why3
[12] François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond. A Simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic. In Bernhard Gramlich, Dale Miller, and Ulrike Sattler, editors, IJCAR 2012: Proceedings of the 6th International Joint Conference on Automated Reasoning, volume 7364 of Lecture Notes in Computer Science, pages 67--81, Manchester, UK, June 2012. Springer. [ bib | DOI | full text on HAL ]
This paper describes a novel decision procedure for quantifier-free linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domain and then proceed either by projection (e.g. Omega-Test) or by branching/cutting methods (branch-and-bound, branch-and-cut, Gomory cuts). Our approach tries to bridge the gap between the two techniques: it interleaves an exhaustive search for a model with bounds inference. These bounds are computed provided an oracle capable of finding constant positive linear combinations of affine forms. We also show how to design an efficient oracle based on the Simplex procedure. Our algorithm is proved sound, complete, and terminating and is implemented in the Alt-Ergo theorem prover. Experimental results are promising and show that our approach is competitive with state-of-the-art SMT solvers.

[11] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.72. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.72 edition, May 2012. [ bib | .pdf ]
Keywords: Why3
[10] François Bobot. Logique de séparation et vérification déductive. Thèse de doctorat, Université Paris-Sud, December 2011. [ bib | full text on HAL | .pdf ]
[9] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. The Why3 platform, version 0.71. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.71 edition, October 2011. https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf. [ bib ]
Keywords: Why3
[8] François Bobot and Andrei Paskevich. Expressing Polymorphic Types in a Many-Sorted Language. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, Frontiers of Combining Systems, 8th International Symposium, Proceedings, volume 6989 of Lecture Notes in Computer Science, pages 87--102, Saarbrücken, Germany, October 2011. [ bib | .pdf ]
[7] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd your herd of provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages, pages 53--64, Wroclaw, Poland, August 2011. https://hal.inria.fr/hal-00790310. [ bib | full text on HAL ]
Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. This article focuses on the former part. Why3 comes with a new enhanced language of logical specification. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.

Keywords: Why3
[6] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.64 edition, February 2011. http://why3.lri.fr/. [ bib ]
Keywords: Why3
[5] François Bobot and Andrei Paskevich. Expressing Polymorphic Types in a Many-Sorted Language, 2011. Preliminary report. http://hal.inria.fr/inria-00591414/. [ bib ]
[4] Clément Hurlin, François Bobot, and Alexander J. Summers. Size does matter : Two certified abstractions to disprove entailment in intuitionistic and classical separation logic. In International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO'09), July 2009. Coq proofs: http://www-sop.inria.fr/everest/Clement.Hurlin/disprove.tgz. [ bib | full text on HAL | .pdf ]
We describe an algorithm to disprove entailment between separation logic formulas. We abstract models of formulas by their size and check whether two formulas have models whose sizes are compatible. Given two formulas A and B that do not have compatible models, we can conclude that A does not entail B. We positi two lift.i://proval.lri.fr/publications/bobot11fan& r/publicatTyp ) sizwe canmulas ,automatirs)>

[11chons="bibtexitem"> François Bobot, Jean-Chrischon, Évelyne Contejean, bib&nchonef="http://dx.doi.org/10.1007/978-3-642-31365-3145/1512464.1512466href="http://hal.inria.fr/hal-0068">Jean-Chrischonummers_chonJean-Chrischonummers_chonJean-Chrischoe Contummers_
[17] François Bobot, bib&n
[4] s="bibtexitem"> François Bobot, Jean-Chrischon, Évelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Guillaume Me, and bib&nalt-ergo">
Back