gondelman.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc gondelman.cite -ob gondelman.bib -c 'author : "gondelman"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../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}
}