François Bobot and Jean-Christophe Filliâtre.
Separation predicates: a taste of separation logic in first-order
In 14th International Conference on Formal Ingineering Methods
(ICFEM), volume 7635 of Lecture Notes in Computer Science, Kyoto,
Japan, November 2012. Springer.
[ bib |
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.
|||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. https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf. [ bib ]|
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala,
Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond.
A Simplex-based extension of Fourier-Motzkin for solving linear
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 |
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.
|||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. https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf. [ bib ]|
|||François Bobot. Logique de séparation et vérification déductive. Thèse de doctorat, Université Paris-Sud, December 2011. [ bib | .pdf ]|
|||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 ]|
|||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 ]|
François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei
Why3: Shepherd your herd of provers.
In Boogie 2011: First International Workshop on Intermediate
Verification Languages, pages 53-64, Wroclaw, Poland, August 2011.
[ bib |
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.
|||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 ]|
|||François Bobot and Andrei Paskevich. Expressing Polymorphic Types in a Many-Sorted Language, 2011. Preliminary report. http://hal.inria.fr/inria-00591414/. [ bib ]|
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.
[ bib |
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 provide two different abstractions (of different precision) of models. Our algorithm is of interest wherever entailment checking is performed (such as in program verifiers).
|||François Bobot, Sylvain Conchon, Évelyne Contejean, and Stéphane Lescuyer. Implementing Polymorphism in SMT solvers. In Clark Barrett and Leonardo de Moura, editors, SMT 2008: 6th International Workshop on Satisfiability Modulo, volume 367 of ACM International Conference Proceedings Series, pages 1-5, 2008. [ bib | DOI | PDF | .pdf | Abstract ]|
|||François Bobot. Satisfiabilité de formules closes modulo une théorie avec égalité et prédicats. Master's thesis, Master Parisien de Recherche en Informatique, 2008. [ bib ]|
|||François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Stéphane Lescuyer, and Alain Mebsout. The Alt-Ergo automated theorem prover, 2008. http://alt-ergo.lri.fr/. [ bib ]|