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{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.lri.fr/}}
}
@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.lri.fr/}}
}
@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.lri.fr/download/manual-0.81.pdf},
  note = {\url{http://why3.lri.fr/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.lri.fr/download/manual-0.82.pdf},
  note = {\url{http://why3.lri.fr/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.lri.fr/download/manual-0.86.1.pdf},
  note = {\url{http://why3.lri.fr/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://proval.lri.fr/publications/bobot12icfem.pdf}
}
@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.lri.fr/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}
}