bobot.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc bobot.cite -ob bobot.bib -c 'author : "bobot"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@misc{marre18colibri,
author = {Bruno Marre and Benjamin Blanc and Patricia Mouy and Zakaria Chihani and Franck Vedrine and Fran\c{c}ois Bobot},
title = {COLIBRI},
howpublished = {System Description at SMTCOMP 2018},
year = 2018,
note = {\url{http://smtcomp.sourceforge.net/2018/systemDescriptions/COLIBRI.pdf}}
}
@inproceedings{chareton21esop,
author = {Chareton, Christophe and Bardin, S{\'e}bastien and Bobot,
Fran{\c{c}}ois and Perrelle, Valentin and Valiron,
Beno{\^i}t},
title = {An Automated Deductive Verification Framework for
Circuit-building Quantum Programs},
booktitle = {Programming Languages and Systems},
year = 2021,
publisher = {Springer-Verlag},
doi = {10.1007/978-3-030-72019-3_6},
url = {https://arxiv.org/pdf/2003.05841.pdf},
pages = {148--177}
}
@article{frama-c-cacm-2021,
author = {Patrick Baudin and Fran{\c{c}}ois Bobot and David B{\"u}hler and Lo{\"i}c Correnson and Florent Kirchner and Nikolai Kosmatov and Andr\'e Maroneze and Valentin Perrelle and Virgile Prevosto and Julien Signoles and Nicky Williams},
title = {The Dogged Pursuit of Bug-Free {C} Programs: The {Frama-C} Software Analysis Platform},
journal = {Communications of the ACM},
year = 2021,
volume = 64,
number = 8,
pages = {56--68},
doi = {10.1145/3470569}
}
@inproceedings{conchon08smt,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean
and St\'ephane Lescuyer},
title = {{Implementing Polymorphism in SMT solvers}},
booktitle = {SMT 2008: 6th International Workshop on Satisfiability Modulo},
pages = {1--5},
year = 2008,
editor = {Clark Barrett and Leonardo de Moura},
volume = 367,
series = {ACM International Conference Proceedings Series},
topics = {team,lri},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {SMT},
x-pdf = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
url = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
isbn = {978-1-60558-440-9},
doi = {10.1145/1512464.1512466},
abstract = {http://www.lri.fr/~contejea/publis/2008smt/abstract.html}
}
@mastersthesis{bobot08master,
author = {Fran\c{c}ois Bobot},
title = {Satisfiabilit\'e de formules closes modulo une th\'eorie avec \'egalit\'e
et pr\'edicats},
school = {Master Parisien de Recherche en Informatique},
topics = {team},
type_publi = {rapport},
type_digiteo = {no},
year = 2008,
x-equipes = {demons PROVAL},
x-type = {master},
x-support = {rapport}
}
@misc{alt-ergo,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala and St\'ephane Lescuyer and Alain Mebsout},
title = {The {Alt-Ergo} Automated Theorem Prover},
note = {\url{http://alt-ergo.lri.fr/}},
topics = {team,lri},
year = 2008,
x-equipes = {demons PROVAL}
}
@inproceedings{HurlinBS09,
author = {Cl\'ement Hurlin and Fran\c{c}ois Bobot and Alexander J. Summers},
title = {Size Does Matter : Two Certified Abstractions to Disprove Entailment in Intuitionistic and Classical Separation Logic},
booktitle = {International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO'09)},
url = {http://www.lri.fr/~bobot/publis/Hurlin_Bobot_Summers_iwaco09.pdf},
note = {Coq proofs: \url{http://www-sop.inria.fr/everest/Clement.Hurlin/disprove.tgz}},
month = jul,
year = {2009},
topics = {team},
abstract = {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).},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-pays = {GB,NL},
hal = {http://hal.inria.fr/hal-00777577}
}
@misc{BobotPaskevich2011,
author = {Fran\c{c}ois Bobot and Andrei Paskevich},
title = {{Expressing Polymorphic Types in a Many-Sorted Language}},
year = 2011,
topics = {team},
note = {Preliminary report. \url{http://hal.inria.fr/inria-00591414/}}
}
@manual{bobot11why3,
title = {The Why3 platform},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.64},
month = feb,
year = 2011,
topics = {team},
keywords = {Why3},
note = {\url{http://why3.org/}}
}
@misc{why3,
title = {The {Why3} platform},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
topics = {team},
keywords = {Why3},
note = {\url{http://why3.org/}}
}
@manual{why3manual071,
title = {The Why3 platform, version 0.71},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.71},
month = oct,
year = 2011,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons PROVAL},
note = {\url{https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf}}
}
@manual{why3manual072,
title = {The Why3 platform, version 0.72},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.72},
month = may,
year = 2012,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons PROVAL},
pdf = {https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf},
rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf}}
}
@manual{why3manual073,
title = {The Why3 platform, version 0.73},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.73},
month = jul,
year = 2012,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons PROVAL},
pdf = {https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf},
rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf}}
}
@manual{why3manual080,
title = {The Why3 platform, version 0.80},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.80},
month = oct,
year = 2012,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons PROVAL},
pdf = {https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf},
note = {\url{https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf}},
rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf}}
}
@manual{why3manual081,
title = {The Why3 platform, version 0.81},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.81},
month = mar,
year = 2013,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons TOCCATA},
pdf = {http://why3.org/download/manual-0.81.pdf},
note = {\url{http://why3.org/download/manual-0.81.pdf}},
hal = {http://hal.inria.fr/hal-00822856/}
}
@manual{why3manual082,
title = {The Why3 platform, version 0.82},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.82},
month = dec,
year = 2013,
topics = {team},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons TOCCATA},
pdf = {http://why3.org/download/manual-0.82.pdf},
note = {\url{http://why3.org/download/manual-0.82.pdf}}
}
@manual{why3manual0861,
title = {The Why3 platform, version 0.86.1},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.86.1},
month = may,
year = 2015,
topics = {team},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons TOCCATA},
pdf = {http://why3.org/download/manual-0.86.1.pdf},
note = {\url{http://why3.org/download/manual-0.86.1.pdf}}
}
@inproceedings{boogie11why3-short,
crossref = {boogie11why3},
booktitle = {Boogie},
address = {},
topics = {}
}
@inproceedings{boogie11why3,
topics = {team},
hal = {http://hal.inria.fr/hal-00790310},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Andrei Paskevich},
title = {Why3: Shepherd Your Herd of Provers},
booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages},
year = 2011,
address = {Wroc\l{}aw, Poland},
month = {August},
pages = {53--64},
note = {\url{https://hal.inria.fr/hal-00790310}},
x-international-audience = {yes},
x-proceedings = {yes},
x-cle-support = {BOOGIE},
x-type = {actes_aux},
x-support = {article},
x-equipes = {demons PROVAL},
keywords = {Why3},
abstract = {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.}
}
@inproceedings{BobotPaskevich2011frocos,
author = {Fran\c{c}ois Bobot and Andrei Paskevich},
title = {{Expressing Polymorphic Types in a Many-Sorted Language}},
pages = {87--102},
topics = {team},
x-type = {article},
x-support = {actes},
x-equipes = {demons PROVAL},
x-cle-support = {FROCOS},
url = {http://proval.lri.fr/publications/bobot11frocos.pdf},
crossref = {frocos11}
}
@inproceedings{BobotPaskevich2011frocos-short,
author = {Fran\c{c}ois Bobot and Andrei Paskevich},
title = {{Expressing Polymorphic Types in a Many-Sorted Language}},
booktitle = {FroCoS},
series = {LNCS},
volume = {6989},
year = {2011},
pages = {87--102}
}
@phdthesis{bobot11these,
author = {Fran\c{c}ois Bobot},
title = {Logique de s\'eparation et v\'erification d\'eductive},
school = {Universit{\'e} Paris-Sud},
type = {Th{\`e}se de Doctorat},
x-tel = {http://tel.archives-ouvertes.fr/docs/00/65/25/08/PDF/VD_BOBOT_FRANCOIS_12122011.pdf},
url = {http://proval.lri.fr/publications/bobot11these.pdf},
hal = {http://tel.archives-ouvertes.fr/tel-00652508},
x-equipes = {demons PROVAL},
x-support = {rapport},
x-type = {these},
topics = {team},
year = 2011,
month = dec
}
@inproceedings{bobot12ijcar,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and
\'Evelyne Contejean and Mohamed Iguernelala and
Assia Mahboubi and Alain Mebsout and Guillaume Melquiond},
title = {A {Simplex}-Based Extension of {Fourier-Motzkin} for
Solving Linear Integer Arithmetic},
booktitle = {IJCAR 2012: Proceedings of the 6th International Joint
Conference on Automated Reasoning},
year = {2012},
editor = {Bernhard Gramlich and Dale Miller and Ulrike Sattler},
series = {Lecture Notes in Computer Science},
address = {Manchester, UK},
month = jun,
volume = {7364},
pages = {67--81},
hal = {http://hal.inria.fr/hal-00687640},
doi = {10.1007/978-3-642-31365-3_8},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
x-cle-support = {IJCAR},
type_publi = {icolcomlec},
publisher = {Springer},
abstract = {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.}
}
@inproceedings{bobot12icfem,
hal = {http://hal.inria.fr/hal-00825088},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre},
title = {Separation Predicates: a Taste of Separation Logic in
First-Order Logic},
booktitle = {14th International Conference on Formal Ingineering Methods
(ICFEM)},
volume = 7635,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
address = {Kyoto, Japan},
month = {November},
year = 2012,
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL},
x-support = {article},
x-cle-support = {ICFEM},
x-type = {actes},
type_publi = {icolcomlec},
topics = {team},
abstract = {This paper introduces \emph{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.},
url = {http://hal.inria.fr/hal-00825088}
}
@inproceedings{bobot13vstte,
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
hal = {http://hal.inria.fr/hal-00875395},
title = {Preserving User Proofs Across Specification Changes},
crossref = {vstte13},
pages = {191--201},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes}
}
@article{bobot14sttt,
topics = {team},
doi = {10.1007/s10009-014-0314-5},
hal_id = {hal-00967132},
hal = {http://hal.inria.fr/hal-00967132/en},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
title = {Let's Verify This with {Why3}},
journal = {International Journal on Software Tools for Technology Transfer (STTT)},
volume = 17,
number = 6,
pages = {709--727},
year = 2015,
note = {See also \url{http://toccata.gitlabpages.inria.fr/toccata/gallery/fm2012comp.en.html}},
publisher = {Springer Berlin / Heidelberg},
x-type = {article},
x-support = {revue},
x-cle-support = {STTT},
x-international-audience = {yes},
x-editorial-board = {yes}
}
@proceedings{frocos11,
editor = {Tinelli, Cesare and Sofronie-Stokkermans, Viorica},
title = {Frontiers of Combining Systems, 8th International Symposium,
FroCoS 2011, Proceedings},
booktitle = {Frontiers of Combining Systems, 8th International Symposium, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6989},
year = {2011},
month = oct,
address = {Saarbr\"ucken, Germany},
isbn = {978-3-642-24363-9},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@proceedings{vstte13,
booktitle = {Verified Software: Theories, Tools, Experiments (5th International Conference VSTTE)},
month = may,
year = 2013,
address = {Atherton, USA},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Ernie Cohen and Andrey Rybalchenko},
series = {Lecture Notes in Computer Science},
volume = {8164},
publisher = {Springer}
}