2011-conference.bib

@comment{{This file has been generated by bib2bib 1.98}}

@comment{{Command line: /usr/bin/bib2bib -q -oc 2011-conference.cite -ob 2011-conference.bib -c 'year = 2011 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{conchon11tacas,
  author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
  title = {{Canonized Rewriting and Ground AC Completion Modulo Shostak Theories}},
  crossref = {tacas2011},
  year = 2011,
  month = apr,
  type_publi = {icolcomlec},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-support = {actes},
  x-cle-support = {TACAS},
  url = {http://proval.lri.fr/publications/conchon11tacas.pdf},
  hal = {http://hal.inria.fr/hal-00777663},
  pages = {45-59},
  doi = {10.1007/978-3-642-19835-9_6},
  abstract = {http://www.lri.fr/~contejea/publis/2011tacas/abstract.html}
}

@inproceedings{benzaken11icde,
  author = {V\'eronique Benzaken and  Jean-Daniel Fekete and Pierre-Luc H\'emery and Wael Khemiri and Ioana Manolescu},
  title = {{EdiFlow: data-intensive interactive workflows for visual analytics}},
  year = {2011},
  booktitle = {{International Conference on Data Engineering (ICDE)}},
  topics = {team},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ICDE},
  x-proceedings = {yes},
  x-international-audience = {yes},
  hal = {http://hal.inria.fr/inria-00532552},
  crossref = {icde11}
}

@inproceedings{contejean11rta,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest
                  and Olivier Pons and Xavier Urbain},
  crossref = {rta11},
  title = {{Automated Certified Proofs with CiME3}},
  x-equipes = {demons PROVAL ext},
  url = {http://drops.dagstuhl.de/opus/volltexte/2011/3119},
  hal = {http://hal.inria.fr/hal-00777669},
  urn = {urn:nbn:de:0030-drops-31192},
  doi = {10.4230/LIPIcs.RTA.2011.21},
  pages = {21--30},
  abstract = {http://www.lri.fr/~contejea/publis/2011rta/abstract.html},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {RTA},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  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}
}

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

@inproceedings{filliatre11jfla,
  author = {Filli\^atre, Jean-Christophe and Kalyanasundaram, Krishnamani},
  title = {Une biblioth\`eque de calcul distribu\'e pour {Objective Caml}},
  topics = {team},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  crossref = {jfla11},
  url = {https://usr.lmf.cnrs.fr/~jcf/publis/jfla-2011.pdf}
}

@inproceedings{MandelPlateau11jfla,
  author = {Louis Mandel and Florence Plateau},
  title = {Typage des horloges p{\'e}riodiques en {Lucy-n}},
  url = {http://www.lri.fr/~mandel/papiers/MandelPlateau-JFLA-2011.pdf},
  abstract = {Lucy-n est un langage permettant de programmer des r{\'e}seaux de
  processus communiquant {\`a} travers des buffers de taille
  born{\'e}e.  La taille des buffers et les rythmes d'ex{\'e}cution relatifs
  des processus sont calcul{\'e}s par une phase de typage appel{\'e}e calcul
  d'horloge. Ce typage n{\'e}cessite la r{\'e}solution d'un ensemble de
  contraintes de sous-typage. L'an dernier, nous avons propos{\'e} un
  algorithme de r{\'e}solution de ces contraintes utilisant des m{\'e}thodes
  issues de l'interpr{\'e}tation abstraite.  Cette ann{\'e}e nous pr{\'e}sentons
  un algorithme tirant profit de toute l'information contenue dans les
  types.},
  topics = {team},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  crossref = {jfla11}
}

@inproceedings{lucy:lctes11,
  author = {Albert Benveniste and Timothy Bourke and
                  Benoit Caillaud and Marc Pouzet},
  title = {{Divide and recycle: types and compilation for a
                   hybrid synchronous language}},
  booktitle = {ACM SIGPLAN/SIGBED Conference on Languages,
               Compilers, Tools and Theory for Embedded Systems (LCTES'11)},
  month = {April},
  address = {Chicago, USA},
  year = 2011,
  url = {lctes11.pdf},
  abstract = {Hybrid modelers such as Simulink have become corner stones of embedded
  systems development.
  They allow both \emph{discrete} controllers and their \emph{continuous}
  environments to be expressed \emph{in a single language}.
  Despite the availability of such tools, there remain a number of issues
  related to the lack of reproducibility of simulations and to the
  separation of the continuous part, which has to be exercised by a
  numerical solver, from the discrete part, which must be guaranteed not to
  evolve during a step.

  Starting from a minimal, yet full-featured, Lustre-like synchronous
  language, this paper presents a conservative extension
  where data-flow equations can be mixed with ordinary differential
  equations (ODEs) with possible reset.
  A type system is proposed to statically distinguish discrete computations
  from continuous ones and to ensure that signals are used in their proper
  domains.
  We propose a semantics based on \emph{non-standard analysis} which gives a
  synchronous interpretation to the whole language, clarifies the
  discrete/continuous interaction and the treatment of zero-crossings, and
  also allows the correctness of the type system to be established.

  The extended data-flow language is realized through a source-to-source
  transformation into a synchronous subset, which can then be compiled using
  existing tools into routines that are both efficient and bounded in their
  use of memory.
  These routines are orchestrated with a single off-the-shelf numerical
  solver using a simple but precise algorithm which treats causally-related
  cascades of zero-crossings.
  We have validated the viability of the approach through experiments with
  the SUNDIALS library.},
  x-type = {article},
  x-support = {actes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  topics = {team}
}

@inproceedings{dross11tap,
  author = {Claire Dross and Jean-Christophe Filli\^atre and Yannick Moy},
  title = {{Correct Code Containing Containers}},
  booktitle = {5th International Conference on Tests and Proofs (TAP'11)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6706},
  pages = {102--118},
  year = 2011,
  address = {Zurich},
  month = jun,
  url = {http://proval.lri.fr/publications/dross11tap.pdf},
  hal = {http://hal.inria.fr/hal-00777683},
  topics = {team},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-equipes = {demons PROVAL ext},
  x-cle-support = {TAP},
  abstract = {
  For critical software development, containers such as lists, vectors, sets or
  maps are an attractive alternative to ad-hoc data structures based on
  pointers.
  As standards like DO-178C put formal verification and testing on an equal
  footing, it is important to give users the ability to apply both to the
  verification of code using containers.
  In this paper,
  we present a definition of containers whose aim is to facilitate their
  use in certified software, using modern proof technology and novel
  specification languages. Correct usage of containers and user-provided
  correctness properties can be checked either by execution during testing
  or by formal proof with an automatic prover.
  We present a formal semantics for containers and an axiomatization of this
  semantics targeted at automatic provers. We have proved in Coq that the
  formal semantics is consistent and that the axiomatization thereof is
  correct.}
}

@inproceedings{filliatre11tfp,
  author = {Jean-Christophe Filli\^atre and Krishnamani Kalyanasundaram},
  title = {Functory: A Distributed Computing Library for {Objective Caml}},
  booktitle = {Trends in Functional Programming},
  year = 2011,
  series = {Lecture Notes in Computer Science},
  volume = {7193},
  pages = {65--81},
  topics = {team},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {TFP},
  x-equipes = {demons PROVAL},
  address = {Madrid, Spain},
  month = {May},
  abstract = {We present Functory, a distributed computing library for
  Objective Caml. The main features of this library
  include (1) a polymorphic API, (2) several implementations to
  adapt to different deployment scenarios such as sequential,
  multi-core or network, and (3) a reliable fault-tolerance mechanism.
  This paper describes the motivation behind this work, as well as
  the design and implementation of the library. It also demonstrates
  the potential of the library using realistic experiments.},
  url = {https://usr.lmf.cnrs.fr/~jcf/publis/tfp11.pdf}
}

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

@inproceedings{mandel11fmcad,
  author = {Louis Mandel and Florence Plateau and Marc Pouzet},
  title = {Static Scheduling of Latency Insensitive Designs with {Lucy-n}},
  booktitle = {Formal Methods in Computer Aided Design ({FMCAD 2011})},
  year = 2011,
  month = oct,
  address = {Austin, TX, USA},
  hal = {http://hal.inria.fr/hal-00654843},
  url = {http://www.lri.fr/~mandel/papiers/MandelPlateauPouzet-FMCAD-2011.pdf},
  webpage = {http://www.lri.fr/~mandel/lucy-n/fmcad11/},
  abstract = {Lucy-n is a dataflow programming language similar to Lustre
  extended with a buffer operator. This language is based on the
  n-synchronous model which was initially introduced for programming
  multimedia streaming applications. In this article, we show that
  Lucy-n is also applicable to model Latency Insensitive
  Designs~(LID). In order to model relay stations, we have to
  introduce a delay operator. Thanks to this new operator, a LID can be
  described by a Lucy-n program. Then, the Lucy-n compiler
  automatically provides static schedules for computation nodes and
  buffer sizes needed in the shell wrappers.},
  topics = {team},
  x-teams = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {FMCAD},
  x-international-audience = {yes},
  x-proceedings = {yes}
}

@inproceedings{BolMel11,
  author = {Sylvie Boldo and Guillaume Melquiond},
  title = {{Flocq}: A Unified Library for Proving Floating-point Algorithms in {Coq}},
  booktitle = {Proceedings of the 20th IEEE Symposium on Computer Arithmetic},
  editor = {Elisardo Antelo and David Hough and Paolo Ienne},
  address = {T{\"u}bingen, Germany},
  year = {2011},
  pages = {243--252},
  doi = {10.1109/ARITH.2011.40},
  hal = {http://hal.archives-ouvertes.fr/inria-00534854/},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ARITH},
  x-international-audience = {yes},
  x-proceedings = {yes}
}

@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{BobotPaskevich2011frocos,
  author = {Fran\c{c}ois Bobot and Andrei Paskevich},
  title = {{Expressing Polymorphic Types in a Many-Sorted Language}},
  pages = {87--102},
  topics = {team},
  x-type = {article},
  x-support = {actes},
  x-equipes = {demons PROVAL},
  x-cle-support = {FROCOS},
  url = {http://proval.lri.fr/publications/bobot11frocos.pdf},
  crossref = {frocos11}
}

@inproceedings{baelde11sofsem,
  author = {David Baelde and
               Romain Beauxis and
               Samuel Mimram},
  title = {Liquidsoap: A High-Level Programming Language for Multimedia
               Streaming},
  crossref = {sofsem11},
  topics = {team, lri},
  type_publi = {colcomlec},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {SOFSEM},
  x-equipes = {demons PROVAL ext},
  year = 2011
}

@inproceedings{benzaken11,
  author = {V\'eronique Benzaken and  Jean-Daniel Fekete and Pierre-Luc H\'emery and Wael Khemiri and Ioana Manolescu},
  title = {{EdiFlow: data-intensive interactive workflows for visual analytics}},
  year = {2011},
  booktitle = {{International Conference on Data Engineering (ICDE)}},
  topics = {team},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  crossref = {icde11}
}

@proceedings{icde11,
  title = {Proceedings of the Twenty Seventh International Conference on
			Data Engineering},
  booktitle = {Proceedings of the Twenty Seventh International Conference on
			Data Engineering},
  editor = {Serge Abiteboul and Christoph Koch and Tan Kian Lee},
  year = 2011,
  month = apr,
  publisher = {{IEEE} Comp. Soc. Press}
}

@proceedings{rta11,
  booktitle = {22nd International Conference on Rewriting Techniques and Applications (RTA 11)},
  series = {Leibniz International Proceedings in Informatics},
  year = {2011},
  volume = {10},
  editor = {Manfred Schmidt-Schau{\ss}},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address = {Novi Sad, Serbia},
  isbn = {978-3-939897-30-9},
  issn = {1868-8969}
}

@proceedings{tacas2011,
  title = {Tools and Algorithms for the Construction and Analysis of Systems},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
  year = 2011,
  month = apr,
  editor = {Parosh A. Abdulla and K. Rustan M. Leino},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6605},
  isbn = {978-3-642-19834-2},
  address = {Saarbr{\"u}cken, Germany}
}

@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{frocos11,
  editor = {Tinelli, Cesare and Sofronie-Stokkermans, Viorica},
  title = {Frontiers of Combining Systems, 8th International Symposium,
               FroCoS 2011, Proceedings},
  booktitle = {Frontiers of Combining Systems, 8th International Symposium, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {6989},
  year = {2011},
  month = oct,
  address = {Saarbr\"ucken, Germany},
  isbn = {978-3-642-24363-9},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes}
}

@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{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{sofsem11,
  editor = {Ivana Cern{\'a} and
               Tibor Gyim{\'o}thy and
               Juraj Hromkovic and
               Keith G. Jeffery and
               Rastislav Kr{\'a}lovic and
               Marko Vukolic and
               Stefan Wolf},
  booktitle = {37th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'11)},
  address = {Nov{\'y} Smokovec, Slovakia},
  title = {SOFSEM 2011: Theory and Practice of Computer Science - 37th
               Conference on Current Trends in Theory and Practice of Computer
               Science},
  publisher = {Springer},
  month = jan,
  series = {Lecture Notes in Computer Science},
  volume = {6543},
  year = {2011},
  isbn = {978-3-642-18380-5},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-editorial-board = {yes},
  x-support = {actes},
  x-pays = {SK}
}