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}
}