gondelman.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -oc gondelman.cite -ob gondelman.bib -c 'author : "gondelman"' /home/marche/biblio/abbrevs.bib /home/marche/biblio/demons.bib /home/marche/biblio/demons2.bib /home/marche/biblio/demons3.bib /home/marche/biblio/team.bib /home/marche/biblio/crossrefs.bib}}
@inproceedings{filliatre14cav,
  author = {Jean-Christophe Filli\^atre and L\'eon
            Gondelman and Andrei Paskevich},
  title = {The Spirit of Ghost Code},
  pages = {1--16},
  crossref = {cav2014},
  topics = {team},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes},
  hal_id = {hal-00873187},
  hal = {http://hal.archives-ouvertes.fr/hal-00873187/en/},
  pdf = {http://hal.archives-ouvertes.fr/hal-00873187/PDF/main.pdf},
  abstract = {
  In the context of deductive program verification, ghost code is part
  of the program that is added for the purpose of specification.
  Ghost code must not interfere with regular code, in the sense that
  it can be erased without any observable difference in the program outcome.
  In particular, ghost data cannot participate in regular
  computations and ghost code cannot mutate regular data or diverge.
  The idea exists in the folklore since the early notion of auxiliary
  variables and is implemented in many state-of-the-art program
  verification tools. However, a rigorous definition and treatment of
  ghost code is surprisingly subtle and few formalizations exist.

  In this article, we describe a simple ML-style programming language
  with mutable state and ghost code.  Non-interference is ensured by a
  type system with effects, which allows, notably, the same data types
  and functions to be used in both regular and ghost code.
  We define the procedure of ghost code erasure and we prove its
  safety using bisimulation.
  A similar type system, with numerous extensions which we briefly discuss,
  is implemented in the program verification environment Why3.
  }
}
@article{gondelman16fmsd,
  author = {Jean-Christophe Filli\^atre and L\'eon
            Gondelman and Andrei Paskevich},
  title = {The Spirit of Ghost Code},
  journal = {Formal Methods in System Design},
  publisher = {Springer},
  year = 2016,
  volume = 48,
  number = 3,
  pages = {152--174},
  issn = {1572-8102},
  doi = {10.1007/s10703-016-0243-x},
  topics = {team},
  hal = {https://hal.archives-ouvertes.fr/hal-01396864v1},
  keywords = {Why3},
  type_publi = {irevcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {revue},
  x-editorial-board = {yes},
  abstract = {
  In the context of deductive program verification, ghost code is part
  of the program that is added for the purpose of specification.
  Ghost code must not interfere with regular code, in the sense that
  it can be erased without observable difference in the program outcome.
  In particular, ghost data cannot participate in regular
  computations and ghost code cannot mutate regular data or diverge.
  The idea exists in the folklore since the early notion of auxiliary
  variables and is implemented in many state-of-the-art program
  verification tools. However, a rigorous definition and treatment of
  ghost code is surprisingly subtle and few formalizations exist.

  In this article, we describe a simple ML-style programming language
  with mutable state and ghost code.  Non-interference is ensured by a
  type system with effects, which allows, notably, the same data types
  and functions to be used in both regular and ghost code.
  We define the procedure of ghost code erasure and we prove its
  safety using bisimulation.
  A similar type system, with numerous extensions which we briefly discuss,
  is implemented in the program verification environment Why3.
  }
}
@phdthesis{gondelman16phd,
  topics = {team},
  title = {A Pragmatic Type System for Deductive Software Verification},
  author = {Gondelman, L{\'e}on},
  hal = {https://tel.archives-ouvertes.fr/tel-01619603},
  school = {Universit{\'e} Paris-Saclay},
  year = 2016,
  type = {Th{\`e}se de Doctorat}
}
@inproceedings{clochard15jfla,
  hal = {https://hal.inria.fr/hal-01094488},
  topics = {team},
  author = {Martin Clochard and L\'eon Gondelman},
  title = {Double {WP}: vers une preuve automatique d'un compilateur},
  crossref = {jfla15}
}
@inproceedings{clochard16,
  topics = {team},
  author = {Martin Clochard and L\'eon Gondelman and M\'ario Pereira},
  title = {The {Matrix} Reproved},
  crossref = {vstte16},
  hal = {https://hal.inria.fr/hal-01316902}
}
@techreport{gondelman16reg,
  topics = {team},
  author = {Jean-Christophe Filli\^atre and L\'eon
            Gondelman and Andrei Paskevich},
  title = {A Pragmatic Type System for Deductive Verification},
  type = {Research Report},
  institution = {Universit\'e Paris Sud},
  year = 2016,
  abstract = { In the context of deductive verication, it is customary
                  today to handle programs with pointers using either
                  separation logic, dynamic frames, or explicit memory
                  models. Yet we can observe that in numerous
                  programs, a large amount of code ts within the scope
                  of Hoare logic, provided we can statically control
                  aliasing. When this is the case, the code
                  correctness can be reduced to simpler verication
                  conditions which do not require any explicit memory
                  model. This makes verication conditions more
                  amenable both to automated theorem proving and to
                  manual inspection and debugging. In this paper, we
                  devise a method of such static aliasing control for
                  a programming language featuring nested data
                  structures with mutable components. Our solution is
                  based on a type system with singleton regions and
                  eects, which we prove to be sound.},
  hal = {https://hal.archives-ouvertes.fr/hal-01256434v3},
  note = {\url{https://hal.archives-ouvertes.fr/hal-01256434v3}}
}
@article{clochard17jar,
  topics = {team},
  title = {The {Matrix} Reproved},
  author = {Clochard, Martin and Gondelman, L{\'e}on and Pereira, M{\'a}rio},
  hal = {https://hal.inria.fr/hal-01617437},
  journal = {Journal of Automated Reasoning},
  pages = {365--383},
  volume = 60,
  number = 3,
  publisher = {Springer},
  year = 2018,
  doi = {10.1007/s10817-017-9436-2}
}
@techreport{fgpps18,
  author = {Jean-Christophe Filli{\^a}tre and L{\'e}on Gondelman and
            Andrei Paskevich and M{\'a}rio Pereira and Sim{\~a}o Melo de Sousa},
  title = {A Toolchain to {P}roduce {C}orrect-by-{C}onstruction {OC}aml
           {P}rograms},
  hal = {https://hal.inria.fr/hal-01783851},
  pdf = {https://hal.inria.fr/hal-01783851/file/main.pdf},
  note = {artifact: \url{https://www.lri.fr/~mpereira/correct_ocaml.ova}},
  year = {2018}
}
@proceedings{cav2014,
  editor = {Armin Biere and Roderick Bloem},
  title = {Computer Aided Verification},
  booktitle = {26th International Conference on Computer Aided Verification},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 8859,
  address = {Vienna, Austria},
  month = jul,
  year = 2014
}
@proceedings{jfla15,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2015,
  booktitle = {Vingt-sixi\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Val d'Ajol, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@proceedings{vstte16,
  booktitle = {8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
  month = jul,
  year = 2016,
  address = {Toronto, Canada},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {VSTTE},
  editor = {Sandrine Blazy and Marsha Chechik},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer}
}