2010-conference.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc 2010-conference.cite -ob 2010-conference.bib -c 'year = 2010 and topics : "team" and $type="inproceedings"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@inproceedings{conchon10lpar,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {{Ground Associative and Commutative Completion Modulo Shostak Theories}},
booktitle = {LPAR, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
year = 2010,
editor = {Andrei Voronkov},
series = {EasyChair Proceedings},
address = {Yogyakarta, Indonesia},
month = oct,
note = {(short paper)},
type_publi = {colloque},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {LPAR}
}
@inproceedings{maneth10vldb,
author = {Sebastian Maneth and
Kim Nguyen},
title = {XPath Whole Query Optimization},
booktitle = {36th International Conference on Very Large Data Bases (VLDB'2010)},
pages = {882--893},
year = 2010,
volume = 3,
number = 1,
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {VLDB}
}
@inproceedings{contejean10pepm,
author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest and Andrei Paskevich and Olivier Pons and Xavier Urbain},
title = {{A3PAT, an Approach for Certified Automated Termination Proofs}},
crossref = {pepm10},
booktitle = {Partial Evaluation and Program Manipulation},
year = 2010,
month = jan,
pages = {63-72},
topics = {team},
x-equipes = {demons PROVAL},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {PEPM},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
topics = {team},
doi = {10.1145/1706356.1706370},
abstract = {http://www.lri.fr/~contejea/publis/2010pepm/abstract.html}
}
@inproceedings{MandelPlateauPouzet-DCC-10,
author = {Louis Mandel and Florence Plateau and Marc Pouzet},
title = {Clock Typing of n-Synchronous Programs},
booktitle = {Designing Correct Circuits ({DCC 2010})},
year = 2010,
month = mar,
address = {Paphos, Cyprus},
topics = {team},
x-equipes = {demons PROVAL},
x-support = {actes_aux},
x-cle-support = {DCCircuits},
x-type = {article},
x-international-audience = {yes},
x-proceedings = {yes},
x-editorial-board = {yes}
}
@inproceedings{lucy:cdc10,
author = {Albert Benveniste and Benoit Caillaud and Marc Pouzet},
title = {{The Fundamentals of Hybrid Systems Modelers}},
booktitle = {49th IEEE International Conference on Decision and
Control (CDC)},
year = {2010},
address = {Atlanta, Georgia, USA},
month = {December 15-17},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {CDC},
x-type = {article}
}
@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}
}
@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{conchon10jfla,
author = {Conchon, Sylvain and Filli\^atre, Jean-Christophe
and Le Fessant, Fabrice and Robert, Julien and Von Tokarski, Guillaume},
title = {{Observation temps-r\'eel de programmes Caml}},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla10},
url = {http://www.lri.fr/~conchon/publis/ocamlviz-jfla2010.pdf}
}
@inproceedings{MandelPlateau10jfla,
author = {Louis Mandel and Florence Plateau and Marc Pouzet},
title = {{Lucy-n}~: une extension n-synchrone de {Lustre}},
url = {http://www.lri.fr/~mandel/papiers/MandelPlateau-JFLA-2010.pdf},
abstract = {Les langages synchrones flot de donn\'ees permettent de programmer
des r\'eseaux de processus communicant sans buffers.
Pour cela, chaque
flot est associ\'e \`a un type d'horloges, qui indique les instants de
pr\'esence de valeurs sur le flot. La communication entre deux
processus \verb+f+ et \verb+g+ peut \^etre faite sans buffer si le
type du flot de sortie de \verb+f+ est \'egal au type du flot d'entr\'ee
de~\verb+g+.
Un syst\`eme de type, le calcul d'horloge, inf\`ere des types tels que
cette condition est v\'erifi\'ee.
Le mod\`ele n-synchrone a pour but de rel\^acher ce mod\`ele de
programmation en autorisant les communications \`a travers des buffers
de taille born\'ee. En pratique, cela consiste \`a introduire une
r\`egle de sous-typage dans le calcul d'horloge.
Nous avons pr\'esent\'e l'ann\'ee derni\`ere un article d\'ecrivant comment
abstraire des horloges pour v\'erifier la relation de
sous-typage. Cette ann\'ee, nous pr\'esentons un langage de
programmation n-synchrone~: Lucy-n. Dans ce langage, l'inf\'erence
des types d'horloges est param\'etrable par l'algorithme de r\'esolution
des contraintes de sous-typage. Nous montrons ici un algorithme
bas\'e sur les travaux de
l'an dernier et comment programmer en Lucy-n \`a travers l'exemple
d'une application de traitement multim\'edia.},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla10}
}
@inproceedings{MandelPlateau10gpl,
author = {Louis Mandel and Florence Plateau and Marc Pouzet},
title = {{Lucy-n~:} une extension n-synchrone de {Lustre}},
booktitle = {{Journ\'ees nationales du GDR-GPL}},
year = {2010},
editor = {\'Eric Cariou and Laurence Duchien and Yves Ledru},
address = {{Pau, France}},
month = mar,
organization = {{GDR GPL}},
topics = {team},
x-equipes = {demons PROVAL},
x-support = {actes_aux},
x-cle-support = {JGDRGPL},
x-type = {article},
annote = {Invited, selected paper}
}
@inproceedings{mandel10jfla,
author = {Louis Mandel},
title = {Cours de {ReactiveML}},
url = {http://www.lri.fr/~mandel/papiers/Mandel-JFLA-2010.pdf},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-support = {actes_aux},
x-type = {article},
x-cle-support = {JFLA},
crossref = {jfla10}
}
@inproceedings{MandelPlateauPouzet-MPC-2010,
author = {Louis Mandel and Florence Plateau and Marc Pouzet},
title = {{Lucy-n}: a n-Synchronous Extension of {Lustre}},
booktitle = {Tenth International Conference on Mathematics of Program Construction ({MPC 2010})},
year = 2010,
month = jun,
address = {Qu{\'e}bec, Canada},
url = {http://www.lri.fr/~mandel/papiers/MandelPlateauPouzet-MPC-10.pdf},
abstract = {Synchronous functional languages such as Lustre
or Lucid Synchrone define a
restricted class of Kahn Process Networks which can be executed with
no buffer.
Every expression is associated to a clock indicating the instants
when a value is present. A dedicated type system, the clock
calculus, checks that the actual clock of a stream equals its
expected clock and thus does not need to be buffered.
The n-synchrony relaxes synchrony by allowing the
communication through bounded buffers whose size is computed at
compile-time.
It is obtained by extending the clock calculus with
a subtyping rule which defines buffering points.
This paper presents the first implementation of the n-synchronous
model inside a Lustre-like language called Lucy-n. The language
extends Lustre with an explicit \verb-buffer- construct whose size
is automatically computed during the clock calculus.
This clock calculus is defined as an inference type system and is
parametrized by the clock language and the algorithm used to solve
subtyping constraints. We detail here one algorithm based on the
abstraction of clocks, an idea originally introduced
in~\cite{Pouzet08c}. The paper presents a simpler, yet more
precise, clock abstraction for which the main algebraic properties have
been proved in Coq. Finally, we illustrate the language on various
examples including a video application.},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {MPC},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{cimatti10date,
author = {Alessandro Cimatti and Anders Franzen and Alberto Griggio and
Krishnamani Kalyanasundaram and Marco Roveri},
title = {Tighter Integration of {BDDs} and {SMT} for Predicate
Abstraction},
hal = {http://hal.inria.fr/inria-00535785},
x-equipes = {demons PROVAL EXT},
x-support = {actes},
x-type = {article},
x-cle-support = {DATE},
topics = {team},
crossref = {date10}
}
@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}
}
@inproceedings{boldo10-nfm,
author = {Sylvie Boldo and Nguyen, Thi Minh Tuyen},
title = {Hardware-independent proofs of numerical programs},
booktitle = {Proceedings of the Second NASA Formal Methods Symposium},
year = 2010,
series = {NASA Conference Publication},
address = {Washington D.C., USA},
month = apr,
x-equipes = {demons PROVAL},
x-support = {actes},
x-cle-support = {NASAFM},
x-type = {article},
topics = {team},
pages = {14--23},
editor = {C\'esar Mu{\~n}oz},
hal = {http://hal.inria.fr/inria-00534410/en/},
x-pdf = {http://shemesh.larc.nasa.gov/NFM2010/proceedings/NASA-CP-2010-216215.pdf},
x-international-audience = {yes},
x-proceedings = {yes},
x-editorial-board = {yes}
}
@inproceedings{boldo10-itp,
author = {Sylvie Boldo and Fran\c{c}ois Cl\'ement and Jean-Christophe Filli\^atre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
title = {Formal Proof of a Wave Equation Resolution Scheme: the Method Error},
booktitle = {Interactive Theorem Proving},
year = 2010,
series = {Lecture Notes in Computer Science},
x-address = {Edinburgh, Scotland},
x-month = jul,
publisher = {Springer},
x-editor = {Matt Kaufmann and Lawrence C. Paulson},
volume = 6172,
pages = {147--162},
hal = {http://hal.inria.fr/inria-00450789/en},
doi = {10.1007/978-3-642-14052-5_12/},
x-equipes = {demons PROVAL ext},
x-support = {actes},
x-cle-support = {ITProving},
x-type = {article},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-editorial-board = {yes}
}
@inproceedings{boldo10-nsv,
author = {Sylvie Boldo},
title = {{Formal verification of numerical programs: from C annotated programs to Coq proofs}},
booktitle = {Proceedings of the Third International Workshop on Numerical Software Verification},
address = {Edinburgh, Scotland},
year = {2010},
month = jul,
x-international-audience = {yes},
x-invited-conference = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
note = {NSV-8},
annote = {Invited paper},
x-equipes = {demons PROVAL},
x-support = {actes_aux},
x-cle-support = {NSV},
x-type = {article},
topics = {team},
hal = {http://hal.inria.fr/inria-00534400/en/}
}
@inproceedings{herms10coq,
author = {Paolo Herms},
title = {Certification of a chain for deductive program verification},
booktitle = {2nd Coq Workshop, satellite of ITP'10},
year = 2010,
x-international-audience = {yes},
x-proceedings = {no},
hal = {http://hal.inria.fr/inria-00535640},
editor = {Yves Bertot},
x-equipes = {demons PROVAL},
x-support = {actes_aux},
x-cle-support = {COQ},
x-type = {article},
topics = {team}
}
@inproceedings{filliatre10-opencert,
author = {Manuel Barbosa and Jean-Christophe Filli\^atre and Jorge Sousa Pinto and B\'arbara Vieira},
title = {A Deductive Verification Platform for Cryptographic Software},
booktitle = {4th International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010)},
year = 2010,
address = {Pisa, Italy},
month = {September},
volume = {33},
publisher = {Electronic Communications of the EASST},
url = {http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/461},
x-equipes = {demons PROVAL ext},
x-support = {actes_aux},
x-cle-support = {OSSC},
x-type = {article},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-pays = {PT}
}
@inproceedings{contejean10gpl,
author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest
and Andrei Paskevich and Olivier Pons and Xavier
Urbain},
title = {{A3PAT, an Approach for Certified Automated Termination Proofs}},
booktitle = {{Journ\'ees nationales du GDR-GPL}},
year = {2010},
editor = {\'Eric Cariou and Laurence Duchien and Yves Ledru},
address = {{Pau, France}},
month = mar,
organization = {{GDR GPL}},
topics = {team},
x-equipes = {demons PROVAL ext},
x-support = {actes_aux},
x-cle-support = {JGDRGPL},
x-type = {article},
annote = {Invited, selected paper}
}
@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{pepm10,
title = {Partial Evaluation and Program Manipulation},
year = 2010,
booktitle = {ACM SIGPLAN 2010 Symposium on Partial Evaluation and Program Manipulation},
editor = {John P. Gallagher and Janis Voigtl{\"a}nder},
address = {Madrid, Spain},
month = jan,
publisher = {ACM Press},
isbn = {978-1-60558-727-1}
}
@proceedings{date10,
title = {Design, Automation \& Test in {E}urope},
year = 2010,
booktitle = {Design, Automation \& Test in {E}urope},
address = {Dresden. Germany},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
month = mar,
publisher = {IEEE}
}
@proceedings{jfla10,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2010,
booktitle = {Vingt-et-uni\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Vieux-Port La Ciotat, France},
publisher = {INRIA},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@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}
}