marche.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc marche.cite -ob marche.bib -c 'author : "Marché"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@inproceedings{boudet96rta,
author = {Alexandre Boudet and \'Evelyne Contejean and Claude
March{\'e}},
title = {{AC}-complete unification and its application to
theorem proving},
topics = {team, cclserver, lri},
year = 1996,
crossref = {rta96},
pages = {18--32},
x-pdf = {http://www.lri.fr/~marche/articles/rta96.ps.gz},
abstract = {http://www.lri.fr/~marche/rta96.html},
doi = {http://dx.doi.org/10.1007/3-540-61464-8_40},
type_publi = {icolcomlec},
clef_labo = {BCM96E}
}
@inproceedings{contejean96rta,
author = {\'Evelyne Contejean and Claude March{\'e}},
title = {{CiME: Completion Modulo $E$}},
crossref = {rta96},
pages = {416--419},
year = 1996,
note = {System Description available at \url{http://cime.lri.fr/}},
x-pdf = {http://www.lri.fr/~marche/articles/cime-rta96.ps.gz},
abstract = {http://www.lri.fr/~marche/cime-rta96.html},
url = {http://cime.lri.fr/},
doi = {http://dx.doi.org/10.1007/3-540-61464-8_70},
type_publi = {icolcomlec},
topics = {team, lri, cclserver},
clef_labo = {CM96E}
}
@techreport{contejean97rr,
author = {\'Evelyne Contejean and Claude March{\'e} and Landy Rabehasaina},
title = {Rewrite systems for natural, integral, and rational
arithmetic},
institution = {Laboratoire de Recherche en Informatique},
year = 1997,
type = {Research Report},
address = {Universit{\'e} de Paris-Sud, Orsay, France}
}
@inproceedings{contejean97rta,
author = {\'Evelyne Contejean and Claude March{\'e} and Landy Rabehasaina},
title = {Rewrite systems for natural, integral, and rational
arithmetic},
pages = {98-112},
crossref = {rta97},
year = 1997,
x-pdf = {http://www.lri.fr/~marche/articles/rta97.ps.gz},
doi = {http://dx.doi.org/10.1007/3-540-62950-5_64},
abstract = {http://www.lri.fr/~marche/rta97.html},
type_publi = {icolcomlec},
topics = {team, lri, cclserver},
clef_labo = {CMR97E}
}
@inproceedings{jouannaud90disco,
topics = {rewriting, old-team},
location = {CM},
author = {Jean-Pierre Jouannaud and Claude March{\'e}},
title = {Completion modulo Associativity, Commutativity and
Identity},
booktitle = {Proc. Int. Symposium on Design and Implementation
of Symbolic Computation Systems, LNCS 429},
year = 1990,
editor = {Alfonso Miola},
publisher = {Springer},
address = {Capri, Italy},
month = apr,
pages = {111--120}
}
@article{jouannaud92tcs,
author = {Jean-Pierre Jouannaud and Claude March{\'e}},
topics = {rewriting, old-team, cclserver},
location = {CM, HC 637},
title = {Termination and completion modulo associativity,
commutativity and identity},
journal = {Theoretical Computer Science},
year = 1992,
volume = 104,
pages = {29--51},
x-pdf = {http://www.lri.fr/~marche/articles/tcs92.ps.gz},
abstract = {http://www.lri.fr/~marche/tcs92.html}
}
@techreport{marche89rr,
author = {Claude March{\'e}},
topics = {rewriting, teamnop},
location = {CM 13},
title = {Compl{\'e}tion modulo Associativit{\'e}, Commutativit{\'e}
et {\'e}l{\'e}ment neutre},
institution = {Laboratoire de Recherche en Informatique},
year = 1989,
type = {Research Report},
number = 513,
address = {Universit{\'e} de Paris-Sud, Orsay, France},
month = sep
}
@techreport{marche90rr,
author = {Claude March{\'e}},
location = {CM 16},
topics = {rewriting, completion, teamnop},
title = {On {AC}-termination and Ground {AC}-completion},
institution = {Laboratoire de Recherche en Informatique},
year = 1990,
type = {Research Report},
number = 598,
address = {Universit{\'e} de Paris-Sud, Orsay, France},
month = oct
}
@techreport{marche91rr,
author = {Claude March{\'e}},
location = {CM,biblio-equipe},
topics = {rewriting, completion, old-teamnop},
title = {The Word Problem of {ACD}-ground Theories is Undecidable},
institution = {Laboratoire de Recherche en Informatique},
year = 1991,
type = {Research Report},
number = 663,
address = {Universit{\'e} de Paris-Sud, Orsay, France},
month = apr
}
@inproceedings{marche91rta,
topics = {rewriting, old-team},
location = {CM},
author = {Claude March{\'e}},
title = {On ground {AC}-completion},
crossref = {rta91},
year = 1991
}
@article{marche92ijfcs,
author = {Claude March{\'e}},
topics = {old-team, cclserver},
location = {CM},
title = {The word problem of {ACD}-ground theories is undecidable},
journal = {International Journal of Foundations of Computer
Science},
year = 1992,
volume = 3,
number = 1,
pages = {81--92},
x-pdf = {http://www.lri.fr/~marche/articles/ijfcs92.ps.gz},
abstract = {http://www.lri.fr/~marche/ijfcs92.html}
}
@misc{marche93litp,
author = {Claude March{\'e}},
title = {Normalized Rewriting -- Application to ground
completion and standard bases},
howpublished = {Notes de cours de l'{\'e}cole de printemps},
year = 1993,
topics = {team, lri},
x-pdf = {http://www.lri.fr/~marche/articles/litp93.ps.gz},
abstract = {http://www.lri.fr/~marche/litp93.html},
type_publi = {diffusion}
}
@phdthesis{marche93these,
author = {Claude March{\'e}},
topics = {team, lri, cclserver},
title = {R{\'e}{\'e}criture modulo une th{\'e}orie
pr{\'e}sent{\'e}e par un syst{\`e}me convergent et
d{\'e}cidabilit{\'e} des probl{\`e}mes du mot dans
certaines classes de th{\'e}ories {\'e}quationnelles},
school = {Universit{\'e} Paris-Sud},
year = 1993,
type = {Th{\`e}se de Doctorat},
address = {Orsay, France},
month = oct,
x-pdf = {http://www.lri.fr/~marche/articles/thesis.ps.gz},
abstract = {http://www.lri.fr/~marche/thesis.html},
type_publi = {these}
}
@inproceedings{marche94lics,
author = {Claude March{\'e}},
topics = {team, lri, cclserver},
title = {Normalised Rewriting and Normalised Completion},
crossref = {lics94},
year = 1994,
pages = {394--403},
x-pdf = {http://www.lri.fr/~marche/articles/lics94.ps.gz},
abstract = {http://www.lri.fr/~marche/lics94.html},
type_publi = {icolcomlec},
clef_labo = {Mar94E}
}
@techreport{marche95lifac,
author = {Claude March{\'e}},
topics = {team, cclserver},
title = {Associative-Commutative Reduction Orderings via
Head-Preserving Interpretations},
institution = {LIFAC},
year = 1995,
number = {95--2},
address = {E.N.S. de Cachan},
month = jan,
x-pdf = {http://www.lri.fr/~marche/articles/lifac-95-2.ps.gz},
abstract = {http://www.lri.fr/~marche/lifac-95-2.html},
type_publi = {diffusion}
}
@inproceedings{marche95litp,
author = {Claude March{\'e}},
topics = {team, lri, cclserver},
title = {Normalized Rewriting -- Application to ground
completion and standard bases},
pages = {154--169},
year = 1995,
crossref = {comon95lncs},
x-pdf = {http://www.lri.fr/~marche/articles/litp93.ps.gz},
abstract = {http://www.lri.fr/~marche/litp93.html},
type_publi = {chapitre},
clef_labo = {Mar95C}
}
@article{marche96jsc,
author = {Claude March{\'e}},
topics = {team, lri, cclserver},
title = {Normalized Rewriting: an alternative to Rewriting
modulo a Set of Equations},
journal = {Journal of Symbolic Computation},
year = 1996,
volume = 21,
number = 3,
pages = {253--288},
x-pdf = {http://www.lri.fr/~marche/articles/jsc96.ps.gz},
abstract = {http://www.lri.fr/~marche/jsc96.html},
type_publi = {irevcomlec},
clef_labo = {Mar96R}
}
@inproceedings{marche95srt,
author = {Claude March{\'e}},
topics = {team, cclserver},
title = {{Normalized Rewriting: an unified view of
Knuth-Bendix completion and Gr{\"o}bner bases computation}},
year = 1995,
crossref = {srt95},
x-pdf = {http://www.lri.fr/~marche/articles/srt95.ps.gz},
abstract = {http://www.lri.fr/~marche/srt95.html},
type_publi = {colloque}
}
@article{marche98pcsal,
author = {Claude March{\'e}},
title = {{Normalized Rewriting: an unified view of
Knuth-Bendix completion and Gr{\"o}bner bases computation}},
journal = {Progress in Computer Science and Applied Logic},
publisher = {Bikha{\"u}ser Verlag},
year = 1998,
volume = 15,
pages = {193--208},
x-pdf = {http://www.lri.fr/~marche/articles/srt95.ps.gz},
abstract = {http://www.lri.fr/~marche/srt95.html},
type_publi = {irevcomlec},
topics = {team, cclserver, lri},
clef_labo = {Mar98R}
}
@inproceedings{marche98rta,
author = {Claude March{\'e} and Xavier Urbain},
title = {Termination of Associative-Commutative Rewriting by Dependency Pairs},
crossref = {rta98},
year = 1998,
pages = {241--255},
x-pdf = {http://www.lri.fr/~marche/articles/rta98.ps.gz},
abstract = {http://www.lri.fr/~marche/rta98.html},
type_publi = {icolcomlec},
topics = {team, lri, cclserver},
clef_labo = {MU98E}
}
@unpublished{contejean96unif,
author = {Alexandre Boudet and {\'E}velyne Contejean and Claude March{\'e}},
title = {{AC Complete Unification and its Application to Theorem Proving}},
note = {UNIF'96},
year = 1996,
address = {Herrsching, Germany},
month = jun
}
@unpublished{duran_sub,
author = {Francisco Duran and Salvador Lucas and
Claude {March\'e} and {Jos\'e} Meseguer and Xavier Urbain},
title = {Termination of Membership Equational Programs},
note = {Submitted}
}
@misc{Caduceus,
title = {The {Caduceus} tool for the verification of {C} programs},
author = {Jean-Christophe Filli\^atre and Thierry Hubert and Claude March\'e},
note = {\url{http://caduceus.lri.fr/}}
}
@techreport{catano03deliv,
author = {N\'estor Cata{\~n}o and Marek Gawkowski and
Marieke Huisman and Bart Jacobs and Claude March{\'e} and Christine Paulin
and Erik Poll and Nicole Rauch and Xavier Urbain},
title = {Logical Techniques for Applet Verification},
institution = {IST VerifiCard Project},
year = 2003,
type = {Deliverable},
number = {5.2},
note = {\url{http://www.cs.kun.nl/VerifiCard/files/deliverables/deliverable_5_2.pdf}},
url = {http://www.cs.kun.nl/VerifiCard/files/deliverables/deliverable_5_2.pdf},
topics = {team}
}
@misc{cime2,
author = {Evelyne Contejean and Claude March{\'e} and
Benjamin Monate and Xavier Urbain},
title = {{CiME version 2}},
note = {Available at
\url{http://cime.lri.fr/}},
year = 2000,
url = {http://cime.lri.fr/},
topics = {team,lri}
}
@inproceedings{jacobs04amast,
author = {Bart Jacobs and Claude March{\'e} and Nicole Rauch},
title = {Formal Verification of a Commercial Smart Card Applet with
Multiple Tools},
crossref = {amast04},
year = 2004,
topics = {team}
}
@techreport{kmu2002rr,
author = {Keiichirou Kusakari and Claude March\'e and Xavier Urbain},
title = {Termination of Associative-Commutative Rewriting using Dependency Pairs Criteria},
institution = {LRI},
year = 2002,
type = {Research Report},
number = 1304,
type_publi = {interne},
topics = {team},
note = {\url{http://www.lri.fr/~urbain/textes/rr1304.ps.gz}},
url = {http://www.lri.fr/~urbain/textes/rr1304.ps.gz}
}
@misc{krakatoa,
author = {Jean-Christophe Filli{\^a}tre and Claude March\'e and Christine Paulin and Xavier Urbain},
title = {The \textsc{Krakatoa} proof tool},
year = 2003,
note = {\url{http://krakatoa.lri.fr/}}
}
@misc{krakatoa02,
author = {Claude March\'e and Christine Paulin and Xavier Urbain},
title = {The \textsc{Krakatoa} proof tool},
year = 2002,
note = {\url{http://krakatoa.lri.fr/}}
}
@inproceedings{FilliatreMarche04,
author = {Jean-Christophe Filli\^atre and Claude March\'e},
title = {{Multi-Prover Verification of C Programs}},
booktitle = {Sixth International Conference on
Formal Engineering Methods},
year = 2004,
publisher = {Springer},
pages = {15--29},
url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus.ps.gz}
}
@inproceedings{contejean03wst,
author = {\'Evelyne Contejean and Claude March{\'e} and Benjamin Monate and Xavier Urbain},
title = {Proving Termination of Rewriting with {\sc C\textit{i}ME}},
crossref = {wst03},
pages = {71--73},
year = 2003,
topics = {team},
type_publi = {icolcomlec},
url = {http://cime.lri.fr}
}
@techreport{contejean04rr,
author = {\'Evelyne Contejean and Claude March{\'e} and Ana-Paula Tom{\'a}s and Xavier Urbain},
title = {Mechanically proving termination using polynomial interpretations},
institution = {LRI},
year = {2004},
type = {Research Report},
number = {1382},
type_publi = {interne},
topics = {team},
url = {http://www.lri.fr/~urbain/textes/rr1382.ps.gz}
}
@article{contejean05jar,
author = {\'Evelyne Contejean and Claude March{\'e} and Ana Paula Tom{\'a}s and Xavier Urbain},
title = {Mechanically proving termination using polynomial
interpretations},
journal = {Journal of Automated Reasoning},
volume = {34},
number = {4},
pages = {325--363},
year = 2005,
type_publi = {irevcomlec},
topics = {team},
doi = {10.1007/s10817-005-9022-x},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {JAR},
abstract = {http://www.lri.fr/~contejea/publis/2005jar/abstract.html}
}
@unpublished{contejean99,
author = {\'Evelyne Contejean and Claude March{\'e} and
Ana-Paola Tom{\'a}s and Xavier Urbain},
title = {Solving Termination Constraints via finite domain polynomial
interpretations},
note = {Unpublished draft, International Workshop on
Constraints in Computational Logics, Gif-sur-Yvette,
France},
year = 1999,
month = sep
}
@inproceedings{duran04pepm,
author = {Francisco Dur{\'a}n and Salvador Lucas and Jos{\'e} Meseguer
and Claude March{\'e} and Xavier Urbain},
title = {Proving Termination of Membership Equational Programs},
crossref = {pepm04},
topics = {team},
type_publi = {icolcomlec}
}
@article{duran06hosc,
author = {Francisco Dur{\'a}n and Salvador Lucas and Jos{\'e} Meseguer
and Claude March{\'e} and Xavier Urbain},
title = {Proving Operational Termination of Membership Equational Programs},
journal = {Higher-Order and Symbolic Computation},
year = 2008,
type_publi = {irevcomlec},
type_digiteo = {revue_cl},
topics = {team},
volume = 21,
number = {1--2},
pages = {59--88},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-editorial-board = {yes},
x-international-audience = {yes},
x-cle-support = {HSC},
x-pdf = {http://www.lri.fr/~marche/duran08hosc.pdf},
hal = {http://hal.inria.fr/inria-00431474/en/},
url = {http://www.lri.fr/~marche/duran08hosc.pdf}
}
@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{filliatre04icfem,
author = {Jean-Christophe Filli{\^a}tre and Claude March{\'e}},
title = {Multi-Prover Verification of {C} Programs},
crossref = {icfem04},
year = {2004},
pages = {15--29},
topics = {team},
type_publi = {icolcomlec},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/caduceus.ps.gz}
}
@inproceedings{filliatre07cav,
author = {Jean-Christophe Filli\^atre and Claude March\'e},
title = {The {Why/Krakatoa/Caduceus} Platform for Deductive Program
Verification},
crossref = {cav07},
pages = {173--177},
topics = {team, lri},
hal = {https://hal.inria.fr/inria-00270820v1},
type_digiteo = {conf_isbn},
type_publi = {icolcomlec},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/cav07.pdf},
x-equipes = {demons PROVAL EXT},
x-type = {articlecourt},
x-support = {actes},
x-cle-support = {CAV},
doi = {10.1007/978-3-540-73368-3_21}
}
@unpublished{hubert05,
author = {Thierry Hubert and Claude March\'e},
title = {A case study of {C} source code verification: the {Schorr}-{Waite} algorithm},
year = 2005,
url = {http://www.lri.fr/~marche/SchorrWaite.ps}
}
@inproceedings{hubert05sefm,
author = {Thierry Hubert and Claude March\'e},
topics = {team},
title = {A case study of {C} source code verification: the {Schorr-Waite} algorithm},
crossref = {sefm05},
type_publi = {icolcomlec},
url = {http://www.lri.fr/~marche/hubert05sefm.ps},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {SEFM}
}
@techreport{hubert07,
author = {Thierry Hubert and Claude March\'e},
title = {Separation Analysis for Deductive Verification},
institution = {Universit\'e Paris XI},
year = 2007,
note = {\url{http://www.lri.fr/~marche/separation.pdf}},
url = {http://www.lri.fr/~marche/separation.pdf},
x-pdf = {http://www.lri.fr/~marche/separation.pdf}
}
@inproceedings{hubert07hav,
author = {Thierry Hubert and Claude March\'e},
title = {Separation Analysis for Deductive Verification},
booktitle = {Heap Analysis and Verification (HAV'07)},
year = 2007,
address = {Braga, Portugal},
month = mar,
topics = {team, lri},
hal = {https://hal.inria.fr/hal-03630177},
type_publi = {icolcomlec},
type_digiteo = {conf_autre},
pages = {81--93},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {HAV}
}
@incollection{marche07,
topics = {team},
author = {Claude March\'e},
title = {Towards Modular Algebraic Specifications for Pointer Programs: a Case Study},
booktitle = {Rewriting, Computation and Proof},
pages = {235--258},
year = 2007,
x-editor = {Hubert Comon-Lundh and Claude Kirchner and H\'el\`ene Kirchner},
volume = 4600,
series = {Lecture Notes in Computer Science},
type_digiteo = {chapitre},
type_publi = {chapitre},
publisher = {Springer},
x-equipes = {demons PROVAL},
x-type = {chapitre},
x-support = {ouvrage}
}
@inproceedings{marche07plpv,
author = {Claude March\'e},
title = {Jessie: an intermediate Language for {Java} and {C} Verification},
booktitle = {Programming Languages meets Program Verification (PLPV)},
year = {2007},
topics = { team},
isbn = {978-1-59593-677-6},
pages = {1--2},
doi = {10.1145/1292597.1292598},
publisher = {ACM Press},
type_digiteo = {conf_isbn},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {actes},
x-cle-support = {PLPV},
address = {Freiburg, Germany}
}
@inproceedings{marche07rta,
author = {March\'e, Claude and Zantema, Hans},
title = {The Termination Competition},
type_digiteo = {conf_isbn},
type_publi = {icolcomlec},
crossref = {rta07},
pages = {303--313},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {RTA},
x-pdf = {http://www.lri.fr/~marche/marche07rta.pdf},
url = {http://www.lri.fr/~marche/marche07rta.pdf},
x-slides = {http://www.lri.fr/~marche/marche07rta-slides.pdf}
}
@inproceedings{marche07wst,
author = {Claude March{\'e} and Hans Zantema and Johannes Waldmann},
title = {The Termination Competition 2007},
crossref = {wst07},
topics = {team},
type_digiteo = {conf_autre},
type_publi = {icolcomlec},
url = {http://www.lri.fr/~marche/termination-competition/},
note = {\url{http://www.lri.fr/~marche/termination-competition/}},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {WST}
}
@article{marche2004jsc,
author = {Claude March\'e and Xavier Urbain},
title = {Modular and Incremental Proofs of {AC}-Termination},
journal = {Journal of Symbolic Computation},
volume = 38,
pages = {873--897},
year = 2004,
topics = {team},
type_digiteo = {revue_cl},
type_publi = {irevcomlec},
url = {http://authors.elsevier.com/sd/article/S074771710400029X}
}
@misc{Ocamlweb,
author = {Jean-Christophe Filli\^atre and Claude March\'e},
title = {{Ocamlweb, a literate programming tool for Objective Caml}},
note = {\url{https://github.com/backtracking/ocamlweb/}},
url = {https://github.com/backtracking/ocamlweb/}
}
@article{marche04jlap,
author = {Claude March{\'e} and Christine Paulin-Mohring and Xavier Urbain},
title = {The \textsc{Krakatoa} Tool for Certification of \textsc{Java/JavaCard} Programs annotated in \textsc{JML}},
journal = {Journal of Logic and Algebraic Programming},
year = 2004,
volume = 58,
number = {1--2},
pages = {89--106},
note = {\url{http://krakatoa.lri.fr}},
url = {http://krakatoa.lri.fr},
ps = {http://www.lri.fr/~marche/marche04jlap.ps},
topics = {team},
type_publi = {irevcomlec}
}
@unpublished{marche04modelejava,
author = {Claude March\'e and Christine Paulin-Mohring},
title = {Reasoning on {Java} Programs with Aliasing and Frame
Conditions},
note = {\url{http://krakatoa.lri.fr/}},
year = 2004
}
@phdthesis{marche05habil,
author = {Claude March\'e},
title = {Preuves m\'ecanis\'ees de propri\'et\'es de programmes},
school = {Universit{\'e} Paris-Sud},
year = 2005,
type = {M\'emoire d'habilitation},
month = dec
}
@phdthesis{marche05hdr,
author = {Claude March{\'e}},
title = {Preuves m{\'e}canis{\'e}es de Propri{\'e}t{\'e}s de Programmes},
year = {2005},
month = dec,
type = {Th\`{e}se d'habilitation},
school = {Universit{\'e} Paris 11},
type_publi = {these},
pdf = {http://www.lri.fr/~marche/marche05hdr.pdf},
x-equipes = {demons PROVAL},
x-type = {habilitation},
x-support = {rapport},
topics = {team, proval}
}
@inproceedings{marche05tphols,
topics = {team},
author = {Claude March\'e and Christine Paulin-Mohring},
title = {Reasoning about {Java} Programs with Aliasing and Frame
Conditions},
crossref = {tphols2005},
pages = {179--194},
topics = {team,lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {TPHOLs},
url = {http://www.lri.fr/~marche/marche05tphols.ps}
}
@inproceedings{marche06sefm,
author = {Claude March\'e and Nicolas Rousset},
topics = {team},
title = {Verification of {Java Card} Applets Behavior with
respect to Transactions and Card Tears},
crossref = {sefm06},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {SEFM}
}
@inproceedings{marche06wst,
author = {Claude March{\'e} and Hans Zantema},
title = {The Termination Competition 2006},
crossref = {wst06},
year = 2006,
topics = {team},
type_publi = {icolcomlec},
url = {http://www.lri.fr/~marche/termination-competition/},
note = {\url{http://www.lri.fr/~marche/termination-competition/}},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {WST}
}
@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}
}
@inproceedings{ohlebusch00rta,
author = {Enno Ohlebusch and Claus Claves and Claude March{\'e}},
title = {{TALP}: A Tool for the Termination Analysis of Logic Programs},
crossref = {rta00},
year = 2000,
pages = {270--273},
topics = {team},
type_publi = {icolcomlec},
url = {http://bibiserv.techfak.uni-bielefeld.de/talp/},
note = {Available at \url{http://bibiserv.techfak.uni-bielefeld.de/talp/}}
}
@inproceedings{ohlebusch03wst,
author = {Enno Ohlebusch and Claus Claves and Claude March{\'e}},
title = {The TALP Tool for Termination Analysis of Logic Programs},
crossref = {wst03},
year = 2003,
topics = {team},
type_publi = {icolcomlec},
url = {http://bibiserv.techfak.uni-bielefeld.de/talp/},
note = {\url{http://bibiserv.techfak.uni-bielefeld.de/talp/}}
}
@techreport{verificard52,
author = {N{\'e}stor {Cata{\~n}o} and M. Gawlowski and Marieke Huisman and Bart Jacobs and Claude March\'e and Christine Paulin and Erik Poll and Nicole Rauch and Xavier Urbain},
title = {Logical Techniques for Applet Verification},
institution = {IST VerifiCard project},
year = 2003,
type = {Deliverable},
number = {5.2},
topics = {team},
type_publi = {rapport}
}
@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}
}
@article{lucas05ipl,
topics = {team},
author = {Salvador Lucas and Claude March\'e and Jos\'e Meseguer},
title = {Operational Termination of Conditional Term Rewriting Systems},
journal = {Information Processing Letters},
publisher = {Elsevier North-Holland, Inc.},
volume = 95,
pages = {446--453},
year = 2005,
type_publi = {irevcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {IPL},
x-international-audience = {yes},
x-language = {en},
abstract = {We describe conditional rewriting by means of an inference system and capture termination as the absence of infinite inference: that is, all proof attempts must either successfully terminate, or they must fail in finite time. We call this notion operational termination. Our notion of operational termination is parametric on the inference system. We prove that operational termination of CTRSs is, in fact, equivalent to a very general notion proposed for 3-CTRSs, namely the notion of quasi-decreasingness, which is currently the most general one which is intended to be checked by comparing parts of the CTRS by means of term orderings. Therefore, existing methods for proving quasi-decreasingness of CTRSs immediately apply to prove operational termination of CTRSs}
}
@techreport{lucas05tr,
author = {Salvador Lucas and Claude March\'e and Jos\'e Meseguer},
title = {Operational Termination of Conditional Term Rewriting Systems},
institution = {Departamento de Sistemas Inform\'aticos y Computaci\'on},
year = 2005,
type = {Research Report},
number = {DSIC II/01/05},
address = {Universidad Polit\'ecnica de Valencia, Spain},
month = feb,
topics = {team},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {rapport}
}
@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}
}
@techreport{tushkanova09rr,
title = {Modular Specification of {Java} Programs},
author = {Tushkanova, Elena and Giorgetti, Alain and
March{\'e}, Claude and Kouchnarenko, Olga},
abstract = {This work investigates the question of modular
specification of generic {Java} classes and
methods. The first part introduces a specification
language for {Java} programs. In the second part the
language is used to specify an array sorting
algorithm by selection. The third and the fourth
parts define a syntax proposal for the specification
a generic {Java} programs, through two examples. The
former is the specification of the generic method
for sorting arrays which comes in the
\texttt{java.util.Arrays} class of the {Java}
{API}. The latter is the specification of the
\texttt{java.util.HashMap} class and its use for
memoization.},
institution = {INRIA},
number = 7097,
year = 2009,
topics = {team},
hal = {http://hal.inria.fr/inria-00434452/en/}
}
@misc{ayad09,
author = {Ali Ayad and Claude March\'e},
title = {Behavioral Properties of Floating-Point Programs},
howpublished = {Hisseo publications},
year = 2009,
note = {\url{http://hisseo.saclay.inria.fr/ayad09.pdf}},
url = {http://hisseo.saclay.inria.fr/ayad09.pdf},
topics = {team}
}
@inproceedings{ayad10ijcar,
author = {Ali Ayad and Claude March\'e},
title = {Multi-Prover Verification of Floating-Point Programs},
crossref = {ijcar10},
pages = {127--141},
hal = {http://hal.inria.fr/inria-00534333},
x-equipes = {demons PROVAL EXT},
topics = {team},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {IJCAR},
x-type = {article},
x-editorial-board = {yes}
}
@techreport{tafat10rr,
title = {A Refinement Approach for Correct-by-Construction Object-Oriented Programs},
author = {Asma Tafat and Sylvain Boulm\'e and Claude March\'e},
institution = {INRIA},
number = 7310,
year = 2010,
x-equipes = {demons PROVAL EXT},
x-support = {rapport},
x-type = {article},
topics = {team},
hal = {http://hal.inria.fr/inria-00491835/en/}
}
@inproceedings{tafat10foveoos,
title = {A Refinement Methodology for Object-Oriented Programs},
author = {Asma Tafat and Sylvain Boulm\'e and Claude March\'e},
crossref = {foveoos10},
x-equipes = {demons PROVAL EXT},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes_aux},
x-type = {article},
x-cle-support = {FOVEOOS},
pages = {143--159},
hal = {http://hal.inria.fr/inria-00534336},
topics = {team}
}
@inproceedings{tafat11foveoos,
title = {A Refinement Methodology for Object-Oriented Programs},
author = {Asma Tafat and Sylvain Boulm\'e and Claude March\'e},
x-equipes = {demons PROVAL EXT},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-type = {article},
x-cle-support = {FOVEOOS},
topics = {team},
pages = {153--167},
hal = {http://hal.inria.fr/inria-00534336},
crossref = {postfoveoos10}
}
@unpublished{bardou09sub,
author = {Romain Bardou and Claude March\'e},
title = {Regions and Permissions for Data Invariants},
institution = {INRIA ARC CeProMi},
note = {Submitted},
year = 2009,
url = {http://www.lri.fr/cepromi/}
}
@unpublished{tafat09sub,
author = {Asma Tafat and Sylvain Boulm\'e and Claude March\'e},
title = {A Refinement Methodology for Object-Oriented Programs},
institution = {INRIA ARC CeProMi},
note = {Submitted},
year = 2010,
url = {http://www.lri.fr/cepromi/}
}
@misc{marche09ws,
author = {Claude March\'e},
title = {The {Krakatoa} tool for Deductive Verification of {Java}
Programs},
howpublished = {Winter School on Object-Oriented Verification,
Viinistu, Estonia},
month = jan,
year = 2009,
url = {http://krakatoa.lri.fr/ws/},
x-pdf = {http://krakatoa.lri.fr/ws/notes.pdf},
note = {\url{http://krakatoa.lri.fr/ws/}},
topics = {team},
x-equipes = {demons PROVAL},
x-support = {diffusion},
x-type = {invitation}
}
@inproceedings{tushkanova10preldta,
author = {Tushkanova, Elena and Giorgetti, Alain and
March{\'e}, Claude and Kouchnarenko, Olga},
title = {Specifying Generic {Java} Programs: two case studies},
booktitle = {PreProceedings of LDTA'2010},
pages = {92--106},
year = 2010,
note = {\url{http://ldta.info/preproceedings2010.pdf}},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes_aux},
x-cle-support = {LDTA},
x-type = {article},
x-editorial-board = {yes}
}
@inproceedings{tushkanova10ldta,
author = {Tushkanova, Elena and Giorgetti, Alain and
March{\'e}, Claude and Kouchnarenko, Olga},
title = {Specifying Generic {Java} Programs: two case studies},
booktitle = {Tenth Workshop on Language Descriptions, Tools and Applications},
editor = {Claus Brabrand and Pierre-Etienne Moreau},
publisher = {ACM Press},
year = 2010,
x-equipes = {demons PROVAL EXT},
topics = {team},
hal = {http://hal.inria.fr/inria-00525784/en/},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {LDTA},
x-type = {article},
x-editorial-board = {yes}
}
@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}
}
@techreport{bardou10rr,
author = {Romain Bardou and Claude March\'e},
title = {Regions and Permissions for Verifying Data Invariants},
institution = {INRIA},
year = 2010,
x-equipes = {demons PROVAL},
x-support = {rapport},
x-type = {article},
topics = {team},
hal = {http://hal.inria.fr/inria-00525384/en/},
note = {\url{http://hal.inria.fr/inria-00525384/en/}},
type = {Research Report},
number = 7412
}
@misc{nguyen10poster,
author = {Nguyen, Thi Minh Tuyen and Boldo, Sylvie and March\'e, Claude},
title = {Formal proofs of numerical programs},
howpublished = {Poster at the Digiteo Forum, Palaiseau, France},
month = oct,
year = 2010,
x-scientific-popularization = {yes},
hal = {http://hal.inria.fr/inria-00536135/en/}
}
@inproceedings{bardou11jfla,
author = {Bardou, Romain and March\'e, Claude},
title = {Perle de preuve: les tableaux creux},
topics = {team},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla11}
}
@misc{bibtex2html10app,
author = {Jean-Christophe Filli\^atre and Claude March\'e},
title = {Bibtex2html},
howpublished = {APP Deposit},
year = 2010,
annote = {\url{https://github.com/backtracking/bibtex2html/}}
}
@article{boldo11mcs,
author = {Sylvie Boldo and Claude March\'e},
title = {Formal verification of numerical programs: from {C} annotated programs to mechanical proofs},
journal = {Mathematics in Computer Science},
topics = {team},
x-type = {article},
x-support = {revue},
x-cle-support = {MCS},
x-equipes = {demons PROVAL},
x-international-audience = {yes},
x-editorial-board = {yes},
year = 2011,
publisher = {Birkhauser Basel},
issn = {1661-8270},
pages = {377--393},
volume = {5},
issue = {4},
doi = {10.1007/s11786-011-0099-9},
hal = {http://hal.inria.fr/hal-00777605}
}
@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.}
}
@techreport{nguyen11rr,
author = {Thi Minh Tuyen Nguyen and Claude March\'e},
title = {Proving Floating-Point Numerical Programs by Analysis of
their Assembly Code},
institution = {INRIA},
year = 2011,
type = {Research Report},
number = 7655,
x-equipes = {demons PROVAL},
x-support = {rapport},
x-type = {article},
topics = {team},
hal = {http://hal.inria.fr/inria-00602266/en/},
note = {\url{http://hal.inria.fr/inria-00602266/en/}}
}
@techreport{kalyan11rr,
title = {Automated Generation of Loop Invariants using Predicate Abstraction},
author = {Kalyanasundaram, Krishnamani and March{\'e}, Claude},
type = {Research Report},
institution = {INRIA},
number = 7714,
year = 2011,
month = aug,
x-equipes = {demons PROVAL},
x-support = {rapport},
x-type = {article},
topics = {team},
hal = {http://hal.inria.fr/inria-00615623/en/},
note = {\url{http://hal.inria.fr/inria-00615623/en/}}
}
@techreport{tafat11rr,
title = {Binary Heaps Formally Verified in {Why3}},
author = {Tafat, Asma and March{\'e}, Claude},
type = {Research Report},
institution = {INRIA},
number = 7780,
year = 2011,
month = oct,
x-equipes = {demons PROVAL},
x-support = {rapport},
x-type = {article},
topics = {team},
keywords = {Why3},
hal = {http://hal.inria.fr/inria-00636083/en/},
note = {\url{http://hal.inria.fr/inria-00636083/en/}}
}
@inproceedings{nguyen11cpp,
author = {Thi Minh Tuyen Nguyen and Claude March\'e},
title = {Hardware-Dependent Proofs of Numerical Programs},
crossref = {cpp2011},
pages = {314--329},
topics = {team},
x-equipes = {demons PROVAL},
x-support = {actes},
x-cle-support = {CPP},
x-type = {article},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
hal = {http://hal.inria.fr/hal-00772508}
}
@inproceedings{herms12vstte,
title = {A Certified Multi-prover Verification Condition Generator},
author = {Paolo Herms and Claude March{\'e} and Benjamin Monate},
crossref = {vstte12},
hal = {http://hal.inria.fr/hal-00639977},
pages = {2--17},
x-equipes = {demons PROVAL ext},
url = {http://proval.lri.fr/publications/herms12vstte.pdf},
topics = {team}
}
@techreport{herms11rr,
title = {A Certified Multi-prover Verification Condition Generator},
author = {Paolo Herms and Claude March{\'e} and Benjamin Monate},
x-equipes = {demons PROVAL ext},
topics = {team},
institution = {INRIA},
year = 2011,
x-support = {rapport},
x-type = {article},
hal = {http://hal.inria.fr/hal-00639977/en/},
note = {\url{http://hal.inria.fr/hal-00639977/en/}},
type = {Research Report},
number = 7793
}
@inproceedings{mentre12abz,
author = {David Mentr\'e and Claude March\'e and Jean-Christophe Filli\^atre and Masashi Asuka},
title = {Discharging Proof Obligations from {Atelier~B} using
Multiple Automated Provers},
booktitle = {ABZ'2012 - 3rd International Conference on Abstract State Machines, Alloy, B and Z},
series = {Lecture Notes in Computer Science},
editor = {Steve Reeves and Elvinia Riccobene},
publisher = {Springer},
volume = {7316},
pages = {238--251},
year = 2012,
address = {Pisa, Italy},
month = jun,
abstract = {We present a method to discharge proof obligations from Atelier~B
using multiple SMT solvers. It is based on a faithful modeling of
B's set theory into polymorphic first-order logic. We report on two
case studies demonstrating a significant improvement in the ratio of
obligations that are automatically discharged.},
obsoletepdf = {https://usr.lmf.cnrs.fr/~jcf/publis/abz12.pdf},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-equipes = {demons PROVAL ext},
x-cle-support = {ABZ},
x-pays = {jp},
hal_id = {hal-00681781},
hal = {http://hal.inria.fr/hal-00681781/en/},
note = {\url{http://hal.inria.fr/hal-00681781/en/}}
}
@inproceedings{bormer11foveoos,
author = {Thorsten Bormer and Marc Brockschmidt and Dino Distefano and Gidon Ernst and Jean-Christophe Filli\^atre and Radu Grigore and Marieke Huisman and Vladimir Klebanov and Claude March\'e and Rosemary Monahan and Wojciech Mostowski and Nadia Polikarpova and Christoph Scheben and Gerhard Schellhorn and Bogdan Tofan and Julian Tschannen and Mattias Ulbrich},
title = {The {COST IC0701} Verification Competition 2011},
url = {http://proval.lri.fr/publications/bormer12foveoos.pdf},
crossref = {postfoveoos11},
x-type = {article},
x-equipes = {demons PROVAL ext},
topics = {team},
hal = {http://hal.inria.fr/hal-00789525}
}
@inproceedings{marche13jfla,
author = {Claude March\'e and Asma Tafat},
title = {Calcul de plus faible pr\'econdition, revisité en {Why3}},
crossref = {jfla13},
topics = {team},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
hal = {http://hal.inria.fr/hal-00778791}
}
@techreport{marche12rr,
title = {Weakest Precondition Calculus, revisited using {Why3}},
author = {Claude March\'e and Asma Tafat},
type = {Research Report},
institution = {INRIA},
number = {RR-8185},
x-equipes = {demons PROVAL},
x-support = {rapport},
x-type = {article},
year = 2012,
month = dec,
topics = {team},
hal = {http://hal.inria.fr/hal-00766171},
pdf = {http://hal.inria.fr/hal-00766171/PDF/RR-8185.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}
}
@inproceedings{clochard14plpv,
hal = {http://hal.inria.fr/hal-00913431},
topics = {team},
author = {Martin Clochard and Claude March\'e and Andrei Paskevich},
title = {Verified Programs with Binders},
booktitle = {Programming Languages meets Program Verification (PLPV)},
year = 2014,
publisher = {ACM Press},
type_digiteo = {conf_isbn},
type_publi = {colloque},
x-equipes = {demons Toccata},
x-support = {actes},
x-cle-support = {PLPV}
}
@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}
}
@article{marche14scp,
topics = {team},
doi = {10.1016/j.scico.2014.04.003},
hal_id = {hal-00967124},
hal = {http://hal.inria.fr/hal-00967124/en},
title = {Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study},
author = {March{\'e}, Claude},
abstract = {We report on a case study that was conducted as part of an industrial research project on static analysis of critical C code. The example program considered in this paper is an excerpt of an industrial code, only slightly modified for confidentiality reasons, involving floating-point computations. The objective was to establish a property on the functional behavior of this code, taking into account rounding errors made during computations. The property is formalized using ACSL, the behavioral specification language available inside the Frama-C environment, and it is verified by automated theorem proving},
publisher = {Elsevier},
journal = {Science of Computer Programming},
year = 2014,
volume = 96,
number = 3,
pages = {279--296},
month = mar,
pdf = {http://hal.inria.fr/hal-00967124/PDF/main.pdf}
}
@inproceedings{delahaye14afadl,
topics = {team},
hal_id = {hal-00998094},
hal = {http://hal.inria.fr/hal-00998094/en/},
title = {Le projet {BWare} : une plate-forme pour la v{\'e}rification automatique d'obligations de preuve {B}},
author = {Delahaye, David and March{\'e}, Claude and Mentr{\'e}, David},
abstract = {Le projet de recherche industrielle BWare (ANR-12-INSE-0010) est financ{\'e} pour 4 ans par le programme \emph{Ing{\'e}nierie Num{\'e}rique \& S{\'e}curit{\'e}} (INS) de l'Agence Nationale de la Recherche (ANR) et a d{\'e}but{\'e} en septembre 2012 (voir le site web du projet : \url{http://bware.lri.fr}). Le consortium du projet BWare associe les partenaires acad{\'e}miques Cedric, LRI, et Inria, ainsi que les partenaires industriels Mitsubishi Electric R\&D Centre Europe (MERCE), ClearSy, et OCamlPro},
booktitle = {Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels (AFADL)},
publisher = {EasyChair},
address = {Paris, France},
audience = {nationale},
year = 2014,
month = jun
}
@inproceedings{delahaye14abz,
topics = {team},
crossref = {abz2014},
hal_id = {hal-00998092},
hal = {http://hal.inria.fr/hal-00998092/en/},
title = {The {BWare} Project: Building a Proof Platform for the Automated Verification of {B} Proof Obligations},
author = {Delahaye, David and Dubois, Catherine and March{\'e}, Claude and Mentr{\'e}, David},
abstract = { We introduce BWare, an industrial research project
that aims to provide a mechanized framework to
support the automated veri cation of proof
obligations coming from the development of
industrial applications using the B method and
requiring high integrity. The methodology adopted
consists in building a generic verification platform
relying on di erent theorem provers, such as rst
order provers and SMT (Satisfiability Modulo
Theories) solvers. Beyond the multi-tool aspect of
our methodology, the originality of this project
also resides in the requirement for the veri cation
tools to produce proof objects, which are to be
checked independently. In this paper, we present
some preliminary results of BWare, as well as some
current major lines of work},
language = {Anglais},
affiliation = {Centre d'Etude et De Recherche en Informatique du Cnam - CEDRIC , TOCCATA - INRIA Saclay - {\^I}le-de-France , Laboratoire de Recherche en Informatique - LRI , Mitsubishi Electric R\&D Centre Europe [France] - MERCE-France},
pages = {290--293}
}
@inproceedings{cfmp14vstte,
hal = {http://hal.inria.fr/hal-01067197},
author = {Martin Clochard and Jean-Christophe
Filli\^atre and Claude March\'e and Andrei Paskevich},
title = {Formalizing Semantics with an Automatic Program
Verifier},
pages = {37--51},
crossref = {vstte14},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes}
}
@article{marche15ercim,
topics = {team},
hal = {http://hal.inria.fr/hal-01102242},
author = {Claude March\'e and Johannes Kanig},
title = {Bridging the Gap between Testing and Formal
Verification in {Ada} Development},
journal = {ERCIM News},
year = 2015,
volume = 100,
pages = {38--39},
month = jan
}
@techreport{dross15rr,
topics = {team},
title = {High-Level Functional Properties of Bit-Level Programs: Formal Specifications and Automated Proofs},
author = {Dross, Claire and Fumex, Cl{\'e}ment and Gerlach, Jens and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-01238376},
type = {Research Report},
number = 8821,
institution = {Inria},
year = 2015,
month = dec
}
@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{fumex16nfm,
topics = {team},
author = {Fumex, Cl\'ement and Dross, Claire and Gerlach, Jens and March\'e, Claude},
title = {Specification and Proof of High-Level Functional Properties of Bit-Level Programs},
pages = {291--306},
crossref = {nfm16},
hal = {https://hal.inria.fr/hal-01314876}
}
@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{chen16rr,
topics = {team},
title = {A Formal Proof of a {Unix} Path Resolution Algorithm},
author = {Ran Chen and Martin Clochard and Claude March\'e},
hal = {https://hal.inria.fr/hal-01406848},
type = {Research Report},
number = {RR-8987},
institution = {Inria},
year = 2016,
month = dec
}
@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}
}
@inproceedings{jeannerod17vstte,
topics = {team},
hal = {https://hal.inria.fr/hal-01534747},
author = {Nicolas Jeannerod and Claude March\'e and Ralf Treinen},
title = {A Formally Verified Interpreter for a Shell-like Programming
Language},
crossref = {vstte17}
}
@techreport{dami17,
topics = {team},
title = {The {CoLiS} language: syntax, semantics and associated tools},
author = {Dami, Ilham and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-01614488},
type = {Technical Report},
number = 0491,
institution = {Inria},
year = 2017,
month = oct
}
@inproceedings{rieuhelft17vstte,
topics = {team},
title = {How to Get an Efficient yet Verified Arbitrary-Precision Integer Library},
author = {Rieu-Helft, Rapha{\"e}l and March{\'e}, Claude and Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-01519732},
booktitle = {9th Working Conference on Verified Software: Theories, Tools, and Experiments},
address = {Heidelberg, Germany},
series = {Lecture Notes in Computer Science},
volume = 10712,
year = 2017,
month = jul,
pages = {84--101},
doi = {10.1007/978-3-319-72308-2_6},
keywords = {arbitrary-precision arithmetic ; deductive program verification ; C language ; Why3 program verifier},
pdf = {https://hal.inria.fr/hal-01519732/file/main.pdf}
}
@article{chen17jfr,
topics = {team},
title = {A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links},
author = {Chen, Ran and Clochard, Martin and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-01652148},
journal = {Journal of Formalized Reasoning},
volume = 10,
number = 1,
year = 2017,
pages = {51--66},
doi = {10.6092/issn.1972-5787/6767},
url = {https://jfr.unibo.it/article/view/6767}
}
@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}
}
@techreport{clochard18rr,
topics = {team},
title = {Deductive Verification via Ghost Debugging},
author = {Clochard, Martin and Paskevich, Andrei and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-01907894},
type = {Research Report},
number = 9219,
institution = {Inria},
year = 2018
}
@inproceedings{clochard20popl,
topics = {team},
title = {Deductive Verification with Ghost Monitors},
author = {Clochard, Martin and March\'e, Claude and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-02368284},
booktitle = {Principles of Programming Languages},
address = {New Orleans, United States},
year = 2020,
doi = {10.1145/3371070}
}
@inproceedings{becker19vstte,
topics = {team},
title = {Ghost Code in Action: Automated Verification of a Symbolic Interpreter},
author = {Becker, Benedikt and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-02276257},
booktitle = {Verified Software: Tools, Techniques and Experiments},
address = {New York, United States},
editor = {Supratik Chakraborty and Jorge A.Navas},
series = {Lecture Notes in Computer Science},
volume = 12031,
year = 2019,
month = jul,
doi = {10.1007/978-3-030-41600-3_8}
}
@techreport{jeannerod19tr,
topics = {team},
title = {Specification of {UNIX} Utilities},
author = {Jeannerod, Nicolas and R{\'e}gis-Gianas, Yann and March{\'e}, Claude and Sighireanu, Mihaela and Treinen, Ralf},
hal = {https://hal.inria.fr/hal-02321691},
type = {Technical Report},
institution = {HAL Archives Ouvertes},
year = 2019,
month = oct
}
@techreport{becker19tr,
topics = {team},
title = {Revision 2 of {CoLiS} language: formal syntax, semantics, concrete and symbolic interpreters},
author = {Becker, Benedikt and March{\'e}, Claude and Jeannerod, Nicolas and Treinen, Ralf},
hal = {https://hal.inria.fr/hal-02321743},
type = {Technical Report},
institution = {HAL Archives Ouvertes},
year = 2019,
month = oct
}
@inproceedings{garchery20jfla,
topics = {team},
title = {Des transformations logiques passent leur certicat},
author = {Garchery, Quentin and Keller, Chantal and March{\'e}, Claude and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-02384946},
crossref = {jfla20}
}
@techreport{becker20rr,
topics = {team},
title = {Rapport d'avancement sur la v{\'e}rification formelle des algorithmes de {ParcourSup}},
author = {Becker, Benedikt and Filli{\^a}tre, Jean-Christophe and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-02447409},
type = {Technical Report},
institution = {Universit{\'e} Paris-Saclay},
year = 2020,
month = jan
}
@inproceedings{becker20tacas,
topics = {team},
title = {Analysing installation scenarios of {Debian} packages},
author = {Becker, Benedikt and Jeannerod, Nicolas and March{\'e}, Claude and R{\'e}gis-Gianas, Yann and Sighireanu, Mihaela and Treinen, Ralf},
hal = {https://hal.archives-ouvertes.fr/hal-02355602},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
series = {Lecture Notes in Computer Science},
volume = 12079,
pages = {235--253},
year = 2020,
doi = {10.1007/978-3-030-45237-7_14}
}
@inproceedings{diverio20vtltc,
topics = {team},
title = {``{You-Know-Why}'': an Early-Stage Prototype of a Key Server Developed using {Why3}},
author = {Diverio, Diego and Belo Louren\c{c}o, Cl{\'a}udio and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-03002187},
booktitle = {VerifyThis Long-term Challenge 2020: Proceedings of the Online-Event},
address = {Dublin, Ireland},
publisher = {Karlsruhe Institute of Technology},
pages = {4--7},
year = 2020,
month = apr,
doi = {10.5445/IR/1000119426}
}
@techreport{belo21rr,
topics = {team},
title = {Formal Analysis of {Ladder} Programs using Deductive Verification},
author = {Belo Louren\c{c}o, Cl{\'a}udio and Cousineau, Denis and Faissole, Florian and March{\'e}, Claude and Mentr{\'e}, David and Inoue, Hiroaki},
hal = {https://hal.inria.fr/hal-03199464},
type = {Research Report},
number = {RR-9402},
institution = {Inria},
year = 2021,
month = apr
}
@techreport{becker21rr,
topics = {team},
title = {Giant-step Semantics for the Categorisation of Counterexamples},
author = {Becker, Benedikt and Belo Louren\c{c}o, Cl{\'a}udio and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-03213438},
type = {Research Report},
number = {RR-9407},
institution = {Inria},
year = 2021,
month = apr
}
@inproceedings{becker21fide,
topics = {team},
title = {Explaining Counterexamples with Giant-Step Assertion Checking},
author = {Becker, Benedikt and Belo Louren\c{c}o, Cl{\'a}udio and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-03217393},
booktitle = {6th Workshop on Formal Integrated Development Environments (F-IDE 2021)},
editor = {Creissac Campos, Jos{\'e} and Paskevich, Andrei},
series = {Electronic Proceedings in Theoretical Computer Science},
doi = {10.4204/EPTCS.338.10},
year = 2021,
month = may
}
@inproceedings{belo21fmics,
topics = {team},
title = {Automated Verification of Temporal Properties of {Ladder} Programs},
author = {Belo Louren{\c c}o, Cl{\'a}udio and Cousineau, Denis and Faissole, Florian and March{\'e}, Claude and Mentr{\'e}, David and Inoue, Hiroaki},
hal = {https://hal.inria.fr/hal-03281580},
booktitle = {Formal Methods for Industrial Critical Systems},
doi = {10.1007/978-3-030-85248-1_2},
series = {Lecture Notes in Computer Science},
volume = 12863,
pages = {21--38},
year = 2021
}
@techreport{denis21rr,
topics = {team},
title = {The {Creusot} Environment for the Deductive Verification of {Rust} Programs},
author = {Denis, Xavier and Jourdan, Jacques-Henri and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-03526634},
type = {Research Report},
number = 9448,
institution = {Inria Saclay - {\^I}le de France},
year = 2021
}
@article{belo22sttt,
topics = {team},
title = {Automated Formal Analysis of Temporal Properties of {Ladder} Programs},
author = {Belo Louren{\c c}o, Cl{\'a}udio and Cousineau, Denis and Faissole, Florian and March{\'e}, Claude and Mentr{\'e}, David and Inoue, Hiroaki},
hal = {https://hal.inria.fr/hal-03737869},
journal = {International Journal on Software Tools for Technology Transfer},
publisher = {Springer},
year = 2022,
pages = {977--997},
volume = 24,
number = 6,
doi = {10.1007/s10009-022-00680-0},
keywords = {Ladder language for programming PLCs ; Timing charts ; Formal specification ; Deductive verification ; Why3 environment}
}
@inproceedings{denis22icfem,
topics = {team},
title = {{Creusot}: a Foundry for the Deductive Verication of {Rust} Programs},
author = {Denis, Xavier and Jourdan, Jacques-Henri and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-03737878},
booktitle = {International Conference on Formal Engineering Methods - ICFEM},
address = {Madrid, Spain},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
year = 2022,
keywords = {Rust programming language ; Deductive program verification ; Aliasing and Ownership ; Prophecies ; Traits}
}
@article{becker22sttt,
topics = {team},
title = {The {CoLiS} Platform for the Analysis of Maintainer Scripts in {Debian} Software Packages},
author = {Becker, Benedikt and Jeannerod, Nicolas and March{\'e}, Claude and R{\'e}gis-Gianas, Yann and Sighireanu, Mihaela and Treinen, Ralf},
hal = {https://hal.inria.fr/hal-03737886},
journal = {International Journal on Software Tools for Technology Transfer},
publisher = {Springer},
year = 2022
}
@inbook{blanchard24acsl,
topics = {team},
hal = {https://inria.hal.science/hal-04265707},
author = {Blanchard, Allan and March\'e, Claude and Prevosto, Virgile},
title = {Guide to Software Verification with {Frama-C} --- Core Components, Usages, and Applications},
chapter = {Formally Expressing what a Program Should Do: the {ACSL} Language},
publisher = {Springer-Verlag},
year = 2024
}
@inproceedings{marche24jfla,
topics = {team},
author = {March{\'e}, Claude and Cousineau, Denis},
hal = {https://inria.hal.science/hal-04342273},
year = 2024,
title = {De l'avantage de nuancer les d{\'e}cisions binaires},
booktitle = {35es Journ{\'e}es Francophones des Langages Applicatifs}
}
@techreport{bonnot23rr,
topics = {team},
author = {Bonnot, Paul and Boyer, Beno\^it and Faissole, Florian and March\'e, Claude and
Rieu-Helft, Rapha\"el},
title = {Formally Verified Bounds on Rounding Errors in Concrete Implementations of Logarithm-Sum-Exponential Functions},
institution = {Inria},
type = {Research Report},
number = 9531,
year = 2023,
hal = {https://inria.hal.science/hal-04343157}
}
@techreport{cousineau24rr,
title = {A Methodological Guide for the Validation of Logic Modelling of {Ladder} Instructions},
author = {Cousineau, Denis and Inoue, Hiroaki and March{\'e}, Claude and Mentr{\'e}, David},
hal = {https://inria.hal.science/hal-04487766},
type = {Technical Report},
number = 0522,
institution = {Inria},
year = 2024
}
@proceedings{comon95lncs,
title = {Term Rewriting},
booktitle = {Term Rewriting},
topics = {team, cclserver},
year = 1995,
editor = {Hubert Comon and Jean-Pierre Jouannaud},
series = {Lecture Notes in Computer Science},
volume = {909},
publisher = {Springer},
organization = {French Spring School of Theoretical Computer
Science},
type_publi = {editeur},
clef_labo = {CJ95}
}
@proceedings{lics94,
title = {Proceedings of the Ninth Annual IEEE Symposium on Logic
in Computer Science},
booktitle = {Proceedings of the Ninth Annual IEEE Symposium on Logic
in Computer Science},
year = 1994,
month = jul,
address = {Paris, France},
publisher = {{IEEE} Comp. Soc. Press}
}
@proceedings{rta91,
title = {4th International Conference on Rewriting Techniques and
Applications},
booktitle = {4th International Conference on Rewriting Techniques and
Applications},
editor = {Ronald. V. Book},
year = 1991,
month = apr,
address = {Como, Italy},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 488
}
@proceedings{rta96,
title = {7th International Conference on Rewriting Techniques and
Applications},
booktitle = {7th International Conference on Rewriting Techniques and
Applications},
editor = {Harald Ganzinger},
publisher = {Springer},
year = 1996,
month = jul,
address = {New Brunswick, NJ, USA},
series = {Lecture Notes in Computer Science},
volume = 1103,
isbn = {3-540-61464-8}
}
@proceedings{rta97,
title = {8th International Conference on Rewriting Techniques and
Applications},
booktitle = {8th International Conference on Rewriting Techniques and
Applications},
editor = {Hubert Comon},
publisher = {Springer},
year = 1997,
month = jun,
address = {Barcelona, Spain},
series = {Lecture Notes in Computer Science},
volume = {1232},
isbn = {3-540-62950-5}
}
@proceedings{rta98,
title = {9th International Conference on Rewriting Techniques and
Applications},
booktitle = {9th International Conference on Rewriting Techniques and
Applications},
editor = {Tobias Nipkow},
publisher = {Springer},
year = 1998,
month = apr,
address = {Tsukuba, Japan},
series = {Lecture Notes in Computer Science},
volume = {1379}
}
@proceedings{rta00,
title = {11th International Conference on Rewriting Techniques and Applications},
booktitle = {11th International Conference on Rewriting Techniques and Applications},
editor = {Leo Bachmair},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 1833,
month = jul,
year = 2000,
address = {Norwich, UK},
isbn = {3-540-67778-X}
}
@proceedings{ijcar10,
title = {International Joint Conference on Automated Reasoning},
booktitle = {Fifth International Joint Conference on Automated Reasoning},
year = 2010,
editor = {J{\"u}rgen Giesl and Reiner H{\"a}hnle},
address = {Edinburgh, Scotland},
month = jul,
series = {Lecture Notes in Artificial Intelligence},
volume = {6173},
publisher = {Springer}
}
@proceedings{srt95,
title = {Proceedings of the Conference on Symbolic Rewriting
Techniques},
booktitle = {Proceedings of the Conference on Symbolic Rewriting
Techniques},
year = 1995,
editor = {Manuel Bronstein and Volker Weispfenning},
address = {Monte Verita, Switzerland}
}
@proceedings{tphols2005,
title = {Theorem Proving in Higher Order Logics:
18th International Conference, TPHOLs 2005},
booktitle = {18th International Conference on Theorem Proving in Higher Order Logics},
editor = {J. Hurd and T. Melham},
series = {Lecture Notes in Computer Science},
year = 2005,
volume = 3603,
addresse = {Oxford, UK},
month = aug,
publisher = {Springer}
}
@proceedings{wst03,
booktitle = {{Extended Abstracts of the 6th International Workshop on Termination, WST'03}},
title = {{Extended Abstracts of the 6th International Workshop on Termination, WST'03}},
year = {2003},
editor = {Albert Rubio},
month = jun,
note = {Technical Report DSIC II/15/03, Universidad Polit\'ecnica de Valencia, Spain}
}
@proceedings{wst06,
booktitle = {{Extended Abstracts of the 8th International Workshop on Termination, WST'06}},
title = {{Extended Abstracts of the 8th International Workshop on Termination, WST'06}},
year = {2006},
editor = {Alfons Geser and Harald Sondergaard},
month = aug
}
@proceedings{wst07,
booktitle = {{Extended Abstracts of the 9th International Workshop on Termination, WST'07}},
title = {{Extended Abstracts of the 9th International Workshop on Termination, WST'07}},
year = {2007},
editor = {Dieter Hofbauer and Alexander Serebrenik},
month = jun
}
@proceedings{amast04,
title = {Algebraic Methodology and Software Technology},
booktitle = {Algebraic Methodology and Software Technology},
year = 2004,
series = {Lecture Notes in Computer Science},
volume = 3116,
address = {Stirling, UK},
month = jul,
publisher = {Springer}
}
@proceedings{pepm04,
title = {Partial Evaluation and Program Manipulation},
year = 2004,
booktitle = {ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation},
address = {Verona, Italy},
month = aug,
publisher = {ACM Press}
}
@proceedings{icfem04,
title = {Formal Engineering Methods},
year = 2004,
booktitle = {6th International Conference on Formal Engineering Methods},
series = {Lecture Notes in Computer Science},
volume = 3308,
editor = {Jim Davies and Wolfram Schulte and Mike Barnett},
address = {Seattle, WA, USA},
month = nov,
publisher = {Springer}
}
@proceedings{cav07,
editor = {Werner Damm and Holger Hermanns},
title = {Computer Aided Verification},
booktitle = {19th International Conference on Computer Aided Verification},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 4590,
address = {Berlin, Germany},
month = jul,
year = {2007}
}
@proceedings{jfla11,
title = {Journ\'ees Francophones des Langages Applicatifs},
editor = {Sylvain Conchon},
year = 2011,
booktitle = {Vingt-deuxi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {La Bresse, France},
publisher = {INRIA},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@proceedings{jfla13,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2013,
booktitle = {Vingt-quatri\`emes Journ\'ees Francophones des Langages Applicatifs},
month = feb,
address = {Aussois, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA}
}
@proceedings{jfla20,
title = {Trente-et-uni\`emes Journ\'ees Francophones des Langages Applicatifs},
booktitle = {Trente-et-uni\`emes Journ{\'e}es Francophones des Langages Applicatifs},
address = {Gruissan, France},
year = 2020,
month = jan,
editor = {Dargaye, Zaynah and R\'egis-Gianas, Yann}
}
@proceedings{sefm05,
title = {Software Engineering and Formal Methods},
year = 2005,
booktitle = {3rd IEEE International Conference on Software Engineering
and Formal Methods (SEFM'05)},
address = {Koblenz, Germany},
editor = {Bernhard K. Aichernig and Bernhard Beckert},
publisher = {{IEEE} Comp. Soc. Press},
month = sep
}
@proceedings{sefm06,
title = {Software Engineering and Formal Methods},
year = 2006,
editor = {Dang Van Hung and Paritosh Pandya},
booktitle = {4th IEEE International Conference on Software Engineering
and Formal Methods (SEFM'06)},
address = {Pune, India},
publisher = {{IEEE} Comp. Soc. Press},
month = sep
}
@proceedings{rta07,
editor = {Franz Baader},
title = {Term Rewriting and Applications},
booktitle = {18th International Conference on Rewriting Techniques and Applications (RTA'07)},
address = {Paris, France},
month = jun,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 4533,
year = 2007
}
@proceedings{foveoos10,
editor = {Bernhard Beckert and Claude March\'e},
title = {Formal Verification of Object-Oriented Software, Papers Presented at the International Conference},
booktitle = {Formal Verification of Object-Oriented Software, Papers Presented at the International Conference},
address = {Paris, France},
month = jun,
series = {Karlsruhe Reports in Informatics},
note = {\url{http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083}},
year = 2010,
hal = {http://hal.inria.fr/hal-00772519},
x-international-audience = {yes},
x-proceedings = {yes},
x-editorial-board = {yes},
x-pays = {DE}
}
@proceedings{postfoveoos10,
editor = {Bernhard Beckert and Claude March\'e},
title = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010},
booktitle = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010},
publisher = {Springer},
topics = {team},
series = {Lecture Notes in Computer Science},
volume = 6528,
month = jan,
year = 2011,
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL ext},
x-support = {actes},
x-type = {edition},
x-cle-support = {FOVEOOS},
x-pays = {DE}
}
@proceedings{postfoveoos11,
editor = {Bernhard Beckert and Ferruccio Damiani and Dilian Gurov},
title = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011},
booktitle = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 7421,
year = 2012,
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {FOVEOOS}
}
@proceedings{cpp2011,
title = {International Conference on Certified Programs and Proofs},
year = 2011,
booktitle = {Certified Programs and Proofs},
editor = {Jean-Pierre Jouannaud and Zhong Shao},
series = {Lecture Notes in Computer Science},
month = dec,
publisher = {Springer}
}
@proceedings{vstte12,
booktitle = {Verified Software: Theories, Tools, Experiments (4th International Conference VSTTE)},
month = jan,
year = 2012,
address = {Philadelphia, USA},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Rajeev Joshi and Peter M{\"u}ller and Andreas Podelski},
series = {Lecture Notes in Computer Science},
volume = 7152,
publisher = {Springer}
}
@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}
}
@proceedings{vstte14,
booktitle = {6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
month = jul,
year = 2014,
address = {Vienna, Austria},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Dimitra Giannakopoulou and Daniel Kroening},
series = {Lecture Notes in Computer Science},
volume = 8471,
publisher = {Springer}
}
@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}
}
@proceedings{abz2014,
booktitle = {Abstract State Machines, Alloy, B, VDM, and Z (ABZ)},
publisher = {Springer},
address = {Toulouse, France},
volume = 8477,
series = {Lecture Notes in Computer Science},
audience = {internationale},
year = 2014,
month = jun
}
@proceedings{nfm16,
booktitle = {8th NASA Formal Methods Symposium},
address = {Minneapolis, MN, USA},
audience = {internationale},
year = 2016,
month = jun,
editor = {Rayadurgam, Sanjai and Tkachuk, Oksana},
series = {Lecture Notes in Computer Science},
volume = {9690},
publisher = {Springer}
}