@comment{{This file has been generated by bib2bib 1.97pl2}}
@comment{{Command line: bib2bib -oc marche.cite -ob marche.bib -c 'topics:"team" and (author : "Marché" or $key="comon01cclbook")' /users/demons/demons/biblio/abbrevs.bib /users/demons/demons/biblio/demons.bib /users/demons/demons/biblio/demons2.bib /users/demons/demons/biblio/demons3.bib /users/demons/demons/biblio/team.bib /users/demons/demons/biblio/crossrefs.bib /users/demons/demons/biblio/crossrefs2.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}
}
@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}
}
@techreport{catano03deliv,
author = {N{\'e}stor 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}
}
@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 = {http://dx.doi.org/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}
}
@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},
url = {http://www.lri.fr/~marche/duran08hosc.pdf}
}
@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 = {http://www.lri.fr/~filliatr/ftp/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},
type_digiteo = {conf_isbn},
type_publi = {icolcomlec},
x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf},
url = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf},
x-equipes = {demons PROVAL EXT},
x-type = {articlecourt},
x-support = {actes},
x-cle-support = {CAV}
}
@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}
}
@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},
type_publi = {icolcomlec},
type_digiteo = {conf_autre},
pages = {81--93},
url = {http://www.lri.fr/~marche/hubert07hav.pdf},
x-pdf = {http://www.lri.fr/~marche/hubert07hav.pdf},
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 = {http://doi.acm.org/10.1145/1292597.1292598},
url = {http://doi.acm.org/10.1145/1292597.1292598},
publisher = {ACM},
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}
}
@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}
}
@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},
url = {http://www.lri.fr/~marche/marche06sefm.ps}
}
@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},
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}
}
@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}
}
@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, \emph{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},
url = {http://www.lri.fr/~marche/ayad10ijcar.pdf},
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},
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},
crossref = {postfoveoos10}
}
@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{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}
}
@inproceedings{herms12vstte,
title = {A Certified Multi-prover Verification Condition Generator},
author = {Paolo Herms and Claude March{\'e} and Benjamin Monate},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL ext},
x-support = {actes},
x-cle-support = {VSTTE},
x-type = {article},
url = {http://proval.lri.fr/publications/herms12vstte.pdf},
topics = {team},
crossref = {vstte12}
}
@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
}
@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}
}
@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 = {http://dx.doi.org/10.1007/s11786-011-0099-9},
url = {http://proval.lri.fr/publications/boldo11mcs.pdf}
}
@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},
note = {\url{http://why3.lri.fr/}}
}
@manual{why3manual071,
title = {The Why3 platform, version 0.71},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.71},
month = oct,
year = 2011,
topics = {team},
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},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons PROVAL},
note = {\url{https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf}}
}
@inproceedings{boogie11why3,
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},
topics = {team},
booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages},
year = 2011,
address = {Wroc\l{}aw, Poland},
month = {August},
url = {http://proval.lri.fr/publications/boogie11final.pdf},
x-international-audience = {yes},
x-proceedings = {yes},
x-cle-support = {BOOGIE},
x-type = {actes_aux},
x-support = {article},
x-equipes = {demons PROVAL},
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, K. 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},
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},
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}
}
@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},
optvolume = {?},
optpages = {?--?},
year = 2012,
address = {Pisa, Italy},
month = {June},
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 = {http://www.lri.fr/~filliatr/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},
topics = {team}
}
@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}
}
@book{comon01cclbook,
booktitle = {Constraints in Computational Logics},
title = {Constraints in Computational Logics},
editor = {Hubert Comon and Claude March{\'e} and Ralf Treinen},
year = 2001,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 2002,
topics = {team},
type_publi = {editeur}
}
@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{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,
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},
todo-volume = {},
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 = {VSTTE},
year = 2012,
editor = {Rajeev Joshi and Peter M{\"u}ller and Andreas Podelski},
series = {Lecture Notes in Computer Science},
publisher = {Springer}
}
This file was generated by bibtex2html 1.97pl2.