moy.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc moy.cite -ob moy.bib -c 'author : "moy"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@inproceedings{lugiez93stacs,
author = {D. Lugiez and J.-L. Moysset},
title = {Complement problems and tree automata in {AC}-like theories},
booktitle = {Proc. Symp. on Theoretical Aspects of Computer
Science},
topics = {disunification, formal_languages},
location = {HC 599, biblio-equipe},
year = 1993,
address = {W{\"u}rzburg},
note = {also available as techincal report {CRIN 92-R-175}}
}
@techreport{lugiez93tr,
author = {D. Lugiez and J.-L. Moysset},
title = {Tree automata help solve formulae in {AC}-theories},
institution = {{CRIN}},
year = 1993,
type = {Research Report},
number = {93-RR-044},
location = {HC 640},
address = {Nancy}
}
@article{lugiez94jsc,
author = {D. Lugiez and J.L. Moysset},
title = {Tree automata help one to solve equational formulae in AC-theories},
journal = {Journal of symbolic computation},
year = 1994,
volume = 11,
number = 1,
location = {biblio-equipe}
}
@inproceedings{boogie11hilite,
author = {J\'er\^ome Guitton and Johannes Kanig and Yannick Moy},
title = {{Why Hi-Lite Ada?}},
booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages},
year = 2011,
address = {Wroc\l{}aw, Poland},
month = {August},
pages = {27--39}
}
@inproceedings{boogie11hilite-short,
author = {J\'er\^ome Guitton and Johannes Kanig and Yannick Moy},
title = {{Why Hi-Lite Ada?}},
booktitle = {Boogie},
year = 2011,
pages = {27--39}
}
@inproceedings{hilite_erts,
author = {Cyrille Comar and Johannes Kanig and Yannick Moy},
title = {Integrating Formal Program Verification with Testing},
booktitle = {Proceedings of the Embedded Real Time Software and Systems conference},
series = {ERTS$^2$ 2012},
year = 2012,
location = {Toulouse, France},
month = feb,
keywords = {GNATprove}
}
@inproceedings{kanig14tap,
title = {Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification},
author = {Kanig, Johannes and Chapman, Rod and Comar, Cyrille and Guitton, Jerôme and Moy, Yannick and Rees, Emyr},
year = 2014,
booktitle = {Tests and Proofs, 8th International Conference},
volume = 8570,
series = {Lecture Notes in Computer Science},
editor = {Seidl, Martina and Tillmann, Nikolai},
doi = {10.1007/978-3-319-09099-3_11},
publisher = {Springer},
pages = {142--157}
}
@inproceedings{dross16rssr,
author = {Claire Dross and Yannick Moy},
title = {Abstract Software Specifications and Automatic Proof of Refinement},
booktitle = {1st International Conference on Reliability, Safety and Security of Railway Systems },
year = 2016
}
@inproceedings{dross17nfm,
author = {Claire Dross and Yannick Moy},
title = {Auto-Active Proof of Red-Black Trees in SPARK},
booktitle = {NASA Formal Methods},
year = 2017
}
@article{DBLP:journals/eceasst/Moy18,
author = {Yannick Moy},
title = {Climbing the Software Assurance Ladder - Practical Formal Verification
for Reliable Software},
journal = {Electron. Commun. Eur. Assoc. Softw. Sci. Technol.},
volume = 76,
year = 2018,
url = {https://doi.org/10.14279/tuj.eceasst.76.1069},
doi = {10.14279/tuj.eceasst.76.1069},
timestamp = {Tue, 25 Aug 2020 16:49:13 +0200},
biburl = {https://dblp.org/rec/journals/eceasst/Moy18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@misc{why12app,
author = {J.-C. Filli\^atre and C. March\'e and Y. Moy and R. Bardou},
title = {Why version 2.30},
howpublished = {APP Deposit},
month = aug,
year = 2012,
note = {IDDN.FR.001.350004.000.S.P.2012.000.10000},
annote = {\url{http://why.lri.fr}}
}
@inproceedings{moy07ccpp,
author = {Yannick Moy},
title = {Union and Cast in Deductive Verification},
booktitle = {Proceedings of the {C/C++} Verification Workshop},
year = 2007,
volume = {Technical Report ICIS-R07015},
month = jul,
pages = {1--16},
publisher = {Radboud University Nijmegen},
x-pdf = {http://www.lri.fr/~moy/Publis/moy07ccpp.pdf},
url = {http://www.lri.fr/~moy/Publis/moy07ccpp.pdf},
type_digiteo = {conf_autre},
type_publi = {icolcomlec},
topics = {team, lri},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes_aux}
}
@inproceedings{moy07hav,
author = {Yannick Moy and Claude March\'e},
title = {Inferring Local (Non-)Aliasing and Strings for Memory Safety},
booktitle = {Heap Analysis and Verification (HAV'07)},
year = 2007,
address = {Braga, Portugal},
month = mar,
pages = {35--51},
topics = {team lri},
type_digiteo = {conf_autre},
type_publi = {icolcomlec},
x-pdf = {http://www.lri.fr/~moy/Publis/moy07hav.pdf},
url = {http://www.lri.fr/~moy/Publis/moy07hav.pdf},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {HAV}
}
@techreport{moy07rr1,
author = {Yannick Moy},
title = {Checking {C} Pointer Programs for Memory Safety},
institution = {INRIA},
year = {2007},
month = oct,
type = {Research Report},
number = {6334},
x-pdf = {http://www.lri.fr/~moy/publis/moy07rr1.pdf},
url = {http://www.lri.fr/~moy/publis/moy07rr1.pdf},
type_digiteo = {no},
type_publi = {rapport},
topics = {team, lri},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {rapport}
}
@inproceedings{moy08vmcai,
author = {Yannick Moy},
title = {Sufficient Preconditions for Modular Assertion Checking},
crossref = {vmcai08},
pages = {188--202},
x-pdf = {http://www.lri.fr/~moy/publis/moy08vmcai.pdf},
url = {http://www.lri.fr/~moy/publis/moy08vmcai.pdf},
topics = {team, lri},
type_digiteo = {conf_isbn},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {VMCAI},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes}
}
@manual{baudin08acsl,
title = {ACSL: ANSI/ISO C Specification Language},
author = {Patrick Baudin and Jean-Christophe Filli\^atre and Claude March\'e and Benjamin Monate and Yannick Moy and Virgile Prevosto},
year = 2008,
note = {\url{http://frama-c.cea.fr/acsl.html}},
url = {http://frama-c.cea.fr/acsl.html},
x-pdf = {http://frama-c.cea.fr/download/acsl_1.4.pdf},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-type = {contrat},
x-support = {rapport}
}
@manual{baudin09acsl,
title = {ACSL: ANSI/ISO C Specification Language, version 1.4},
author = {Patrick Baudin and Jean-Christophe Filli\^atre and Claude March\'e and Benjamin Monate and Yannick Moy and Virgile Prevosto},
year = 2009,
note = {\url{http://frama-c.cea.fr/acsl.html}},
url = {http://frama-c.cea.fr/acsl.html},
x-pdf = {http://frama-c.cea.fr/download/acsl_1.4.pdf},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-type = {contrat},
x-support = {rapport}
}
@manual{baudin20acsl,
title = {ACSL: ANSI/ISO C Specification Language, version 1.16},
author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filli\^atre and Claude March\'e and Benjamin Monate and Yannick Moy and Virgile Prevosto},
year = 2020,
url = {https://frama-c.com/html/acsl.html},
topics = {team}
}
@phdthesis{moy09phd,
author = {Yannick Moy},
title = {Automatic Modular Static Safety Checking for C Programs},
school = {Universit{\'e} Paris-Sud},
year = 2009,
month = jan,
topics = {team},
x-equipes = {demons PROVAL},
x-type = {these},
x-support = {rapport},
url = {http://www.lri.fr/~marche/moy09phd.pdf}
}
@manual{moy08manual,
title = {Jessie Plugin Tutorial, \emph{Lithium} version},
author = {Yannick Moy and Claude March\'e},
organization = {INRIA},
year = 2008,
note = {\url{http://www.frama-c.cea.fr/jessie.html}},
url = {http://www.frama-c.cea.fr/jessie.html},
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion},
x-pdf = {http://www.frama-c.cea.fr/jessie/main.pdf}
}
@manual{moy09manual,
title = {Jessie Plugin Tutorial, \emph{Beryllium} version},
author = {Yannick Moy and Claude March\'e},
organization = {INRIA},
year = 2009,
note = {\url{http://www.frama-c.cea.fr/jessie.html}},
url = {http://www.frama-c.cea.fr/jessie.html},
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion},
x-pdf = {http://www.frama-c.cea.fr/jessie/main.pdf}
}
@manual{moy10manual,
title = {Jessie Plugin, Boron version},
author = {Yannick Moy and Claude March\'e},
organization = {INRIA},
year = 2010,
note = {\url{http://frama-c.com/jessie/jessie-tutorial.pdf}},
url = {http://frama-c.com/jessie/jessie-tutorial.pdf},
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion},
x-pdf = {http://frama-c.com/jessie/jessie-tutorial.pdf}
}
@manual{moy11jessie,
title = {The Jessie plugin
for Deduction Verification in Frama-C --- Tutorial and Reference Manual},
author = {Yannick Moy and Claude March\'e},
organization = {INRIA \& LRI},
year = 2011,
note = {\url{http://krakatoa.lri.fr/}},
url = {http://krakatoa.lri.fr},
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion},
x-pdf = {http://krakatoa.lri.fr/jessie.pdf}
}
@article{moy10jsc,
author = {Yannick Moy and Claude March\'e},
title = {Modular Inference of Subprogram Contracts for Safety Checking},
journal = {Journal of Symbolic Computation},
year = 2010,
volume = 45,
hal = {http://hal.inria.fr/inria-00534331/en/},
doi = {10.1016/j.jsc.2010.06.004},
x-international-audience = {yes},
x-editorial-board = {yes},
pages = {1184-1211},
x-equipes = {demons PROVAL ext},
x-support = {revue},
x-cle-support = {JSC},
x-type = {article},
topics = {team}
}
@inproceedings{dross11tap,
author = {Claire Dross and Jean-Christophe Filli\^atre and Yannick Moy},
title = {{Correct Code Containing Containers}},
booktitle = {5th International Conference on Tests and Proofs (TAP'11)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6706},
pages = {102--118},
year = 2011,
address = {Zurich},
month = jun,
url = {http://proval.lri.fr/publications/dross11tap.pdf},
hal = {http://hal.inria.fr/hal-00777683},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-equipes = {demons PROVAL ext},
x-cle-support = {TAP},
abstract = {
For critical software development, containers such as lists, vectors, sets or
maps are an attractive alternative to ad-hoc data structures based on
pointers.
As standards like DO-178C put formal verification and testing on an equal
footing, it is important to give users the ability to apply both to the
verification of code using containers.
In this paper,
we present a definition of containers whose aim is to facilitate their
use in certified software, using modern proof technology and novel
specification languages. Correct usage of containers and user-provided
correctness properties can be checked either by execution during testing
or by formal proof with an automatic prover.
We present a formal semantics for containers and an axiomatization of this
semantics targeted at automatic provers. We have proved in Coq that the
formal semantics is consistent and that the axiomatization thereof is
correct.}
}
@techreport{hauzar16rr,
topics = {team},
title = {Counterexamples from proof failures in the {SPARK} program verifier},
author = {Hauzar, David and March{\'e}, Claude and Moy, Yannick},
hal = {https://hal.inria.fr/hal-01271174},
type = {Research Report},
number = {RR-8854},
institution = {Inria Saclay Ile-de-France},
year = 2016,
month = feb
}
@inproceedings{hauzar16sefm,
topics = {team},
author = {Hauzar, David and March\'e, Claude and Moy, Yannick},
title = {Counterexamples from Proof Failures in {SPARK}},
booktitle = {Software Engineering and Formal Methods},
year = 2016,
pages = {215--233},
doi = {10.1007/978-3-319-41591-8_15},
editor = {De Nicola, Rocco and Eva K\"uhn},
series = {Lecture Notes in Computer Science},
address = {Vienna, Austria},
hal = {https://hal.inria.fr/hal-01314885}
}
@inproceedings{kosmatov16isola,
topics = {team},
title = {Static versus Dynamic Verification in {Why3}, {Frama-C} and {SPARK
2014}},
author = {Kosmatov, Nikolai and March{\'e}, Claude and Moy, Yannick and
Signoles, Julien},
hal = {https://hal.inria.fr/hal-01344110},
booktitle = {7th International Symposium on Leveraging Applications of Formal
Methods, Verification and Validation (ISoLA)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
year = 2016,
pages = {461--478},
volume = {9952},
editor = {Tiziana Margaria and Bernhard Steffen},
address = {Corfu, Greece},
month = oct,
doi = {10.1007/978-3-319-47166-2_32}
}
@techreport{fumex17rr,
topics = {team},
title = {Automated Verification of Floating-Point Computations in {Ada}
Programs},
author = {Fumex, Cl{\'e}ment and March{\'e}, Claude and Moy, Yannick},
hal = {https://hal.inria.fr/hal-01511183},
type = {Research Report},
number = {RR-9060},
pages = 53,
institution = {Inria},
year = 2017,
month = apr
}
@inproceedings{fumex17vstte,
topics = {team},
hal = {https://hal.inria.fr/hal-01534533/},
author = {Cl\'ement Fumex and Claude March\'e and Yannick Moy},
title = {Automating the Verification of Floating-Point Programs},
crossref = {vstte17}
}
@article{dailler18jlamp,
topics = {team},
title = {Instrumenting a Weakest Precondition Calculus for Counterexample Generation},
author = {Dailler, Sylvain and Hauzar, David and March{\'e}, Claude and Moy, Yannick},
hal = {https://hal.inria.fr/hal-01802488},
journal = {Journal of Logical and Algebraic Methods in Programming},
publisher = {Elsevier},
volume = 99,
pages = {97--113},
year = 2018,
doi = {10.1016/j.jlamp.2018.05.003},
keywords = {Deductive Program Verification ; Weakest Precondition Calculus ; Satisfiability Modulo Theories ; Counterexamples}
}
@inproceedings{dailler2018,
topics = {team},
hal = {https://hal.inria.fr/hal-01936302},
author = {Dailler, Sylvain and March{\'e}, Claude and Moy, Yannick},
title = {Lightweight Interactive Proving inside an Automatic Program
Verifier},
booktitle = {Proceedings of the Fourth Workshop on Formal Integrated
Development Environment, F-IDE, Oxford, UK,
July 14, 2018},
year = {2018},
doi = {10.4204/EPTCS.284.1}
}
@unpublished{jaloyan18,
topics = {team},
title = {Verification of Programs with Pointers in {SPARK}},
author = {Jaloyan, Georges-Axel and Dross, Claire and Maalej, Maroua and Moy, Yannick and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-01936105},
note = {working paper \url{https://hal.inria.fr/hal-01936105}},
year = 2018,
month = nov
}
@inproceedings{jaloyan20icfem,
topics = {team},
title = {Verification of Programs with Pointers in {SPARK}},
author = {Jaloyan, Georges-Axel and Dross, Claire and Maalej, Maroua and Moy, Yannick and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-03094566},
booktitle = {Formal Methods and Software Engineering (ICFEM)},
pages = {55--72},
year = 2020,
doi = {10.1007/978-3-030-63406-3\_4}
}
@proceedings{vmcai08,
editor = {Francesco Logozzo and Doron Peled and Lenore Zuck},
title = {Verification, Model Checking, and Abstract Interpretation},
booktitle = {9th International Conference on Verification, Model Checking, and Abstract Interpretation},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 4905,
address = {San Francisco, California, USA},
month = jan,
year = {2008}
}
@proceedings{vstte17,
topics = {team},
hal = {https://hal.inria.fr/hal-01670145},
title = {Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference {VSTTE}},
booktitle = {Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference {VSTTE}},
month = dec,
year = 2017,
address = {Heidelberg, Germany},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Andrei Paskevich and Thomas Wies},
series = {Lecture Notes in Computer Science},
number = 10712,
publisher = {Springer}
}