2009-conference.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc 2009-conference.cite -ob 2009-conference.bib -c 'year = 2009 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{lucy:lctes09,
  author = {Paul Caspi and Jean-Louis Cola\c{c}o and L\'eonard G\'erard
                  and Marc Pouzet and Pascal Raymond},
  title = {{Synchronous Objects with Scheduling Policies}:
                   Introducing safe shared memory in {Lustre}},
  year = {2009},
  month = jun,
  address = {Dublin},
  booktitle = {ACM International Conference on
                  Languages, Compilers, and Tools for Embedded Systems
                  (LCTES)},
  x-type = {article},
  topics = {team},
  x-support = {actes},
  x-equipes = {demons PROVAL ext}
}
@inproceedings{lucy:emsoft09,
  author = {Marc Pouzet and Pascal Raymond},
  title = {Modular Static Scheduling of Synchronous Data-flow
                  Networks: An efficient symbolic representation},
  booktitle = {ACM International Conference on
                  Embedded Software (EMSOFT'09)},
  address = {Grenoble, France},
  month = {October},
  year = 2009,
  topics = {team},
  x-type = {article},
  x-support = {actes},
  x-equipes = {demons PROVAL ext}
}
@inproceedings{filliatre09afm,
  author = {Jean-Christophe Filli\^atre},
  title = {{Invited tutorial: Why --- an intermediate language for deductive program verification}},
  booktitle = {{Automated Formal Methods (AFM09)}},
  editor = {Hassen Sa\"{\i}di and Natarajan Shankar},
  year = 2009,
  topics = { team},
  type_digiteo = {conf_autre},
  type_publi = {colloque},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-invited-conference = {yes},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-support = {actes},
  x-cle-support = {AFM},
  address = {Grenoble, France}
}
@inproceedings{MandelPlateau09_HFL,
  address = {York, UK},
  author = {Albert Cohen and Louis Mandel and Florence Plateau and Marc Pouzet},
  booktitle = {Hardware Design using Functional languages (HFL 09)},
  month = mar,
  title = {Relaxing Synchronous Composition with Clock Abstraction},
  year = {2009},
  pages = {35-52},
  x-international-audience = {yes},
  x-proceedings = {yes},
  topics = {team},
  x-support = {actes_aux},
  x-equipes = {demons PROVAL alchemy},
  x-type = {article},
  type_publi = {icolcomlec}
}
@inproceedings{mlpost09jfla,
  author = {Romain Bardou and Jean-Christophe Filli\^atre and Johannes Kanig and St\'ephane Lescuyer},
  title = {{Faire bonne figure avec Mlpost}},
  url = {https://usr.lmf.cnrs.fr/~jcf/publis/mlpost-fra.pdf},
  abstract = {Cet article pr\'esente Mlpost, une biblioth\`eque Ocaml de dessin
  scientifique. Elle s'appuie sur Metapost, qui permet notamment
  d'inclure des fragments \LaTeX\ dans les figures. Ocaml offre une
  alternative s\'eduisante aux langages de macros \LaTeX, aux langages
  sp\'ecialis\'es ou m\^eme aux outils graphiques. En particulier,
  l'utilisateur de Mlpost b\'en\'eficie de toute l'expressivit\'e
  d'Ocaml et de son typage statique. Enfin Mlpost propose un style
  d\'eclaratif qui diff\`ere de celui, souvent imp\'eratif, des outils existants.},
  topics = {team, lri},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  crossref = {jfla09}
}
@inproceedings{mandel-plateau09jfla,
  author = {Louis Mandel and Florence Plateau},
  title = {{Abstraction d'horloges dans les syst\`emes synchrones flot de donn\'ees}},
  url = {http://www.lri.fr/~plateau/papers/jfla09.pdf},
  abstract = {Les langages synchrones flot de donn\'ees tels que
                  Lustre manipulent des s\'equences infinies de
                  donn\'ees comme valeurs de base.  Chaque flot est
                  associ\'e \`a une horloge qui d\'efinit les instants
                  o\`u sa valeur est pr\'esente. Cette horloge est une
                  information de type et un syst\`eme de types
                  d\'edi\'e, le calcul d'horloges, rejette
                  statiquement les programmes qui ne peuvent pas \^etre
                  ex\'ecut\'es de mani\`ere synchrone. Dans les
                  langages synchrones existants, cela revient \`a se
                  demander si deux flots ont la m\^eme horloge et repose
                  donc uniquement sur l'\'egalit\'e d'horloges.  Des
                  travaux r\'ecents ont montr\'e l'int\'er\^et
                  d'introduire une notion rel\^ach\'ee du synchronisme,
                  o\`u deux flots peuvent \^etre compos\'es d\`es qu'ils
                  peuvent \^etre synchronis\'es par l'introduction d'un
                  buffer de taille born\'ee (comme c'est fait dans le
                  mod\`ele SDF d'Edward Lee). Techniquement, cela
                  consiste \`a remplacer le typage par du
                  sous-typage. Ce papier est une traduction et
                  am\'elioration technique de~\cite{Pouzet08c} qui pr\'esente
                  un moyen simple de mettre en oeuvre ce mod\`ele
                  rel\^ach\'e par l'utilisation d'horloges abstraites.
                  Les valeurs abstraites repr\'esentent des ensembles
                  d'horloges concr\`etes qui ne sont pas
                  n\'ecessairement p\'eriodiques.  Cela permet de
                  mod\'eliser divers aspects des logiciels
                  temps-r\'eel embarqu\'es, tels que la gigue born\'ee
                  pr\'esente dans les syst\`emes vid\'eo, le temps
                  d'ex\'ecution des processus temps r\'eel et, plus
                  g\'en\'eralement, la communication \`a travers des
                  buffers de taille born\'ee.  Nous pr\'esentons ici
                  l'alg\`ebre des horloges abstraites et leurs
                  principales propri\'et\'es th\'eoriques.},
  topics = {team, lri},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  crossref = {jfla09}
}
@inproceedings{boldo09calculemus,
  author = {Sylvie Boldo and Jean-Christophe Filli\^atre and Guillaume Melquiond},
  title = {Combining {C}oq and {G}appa for {C}ertifying {F}loating-{P}oint
  {P}rograms },
  booktitle = {16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning},
  pages = {59--74},
  year = {2009},
  month = jul,
  volume = {5625},
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  address = {Grand Bend, Canada},
  doi = {10.1007/978-3-642-02614-0_10},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-support = {actes},
  topics = {team}
}
@inproceedings{boldo09icalp,
  author = {Sylvie Boldo},
  title = {Floats and Ropes: A Case Study for Formal Numerical Program Verification},
  booktitle = {36th International Colloquium on Automata, Languages and Programming},
  pages = {91--102},
  year = {2009},
  volume = {5556},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-support = {actes},
  topics = {team},
  doi = {10.1007/978-3-642-02930-1_8},
  x-url = {http://fost.saclay.inria.fr/files/icalp2009trackb_submission_48.pdf}
}
@inproceedings{HurlinBS09,
  author = {Cl\'ement Hurlin and Fran\c{c}ois Bobot and Alexander J. Summers},
  title = {Size Does Matter : Two Certified Abstractions to Disprove Entailment in Intuitionistic and Classical Separation Logic},
  booktitle = {International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO'09)},
  url = {http://www.lri.fr/~bobot/publis/Hurlin_Bobot_Summers_iwaco09.pdf},
  note = {Coq proofs: \url{http://www-sop.inria.fr/everest/Clement.Hurlin/disprove.tgz}},
  month = jul,
  year = {2009},
  topics = {team},
  abstract = {We describe an algorithm to disprove entailment between
	     separation logic formulas. We abstract models
	     of formulas by their size and check whether two formulas
	     have models whose sizes are compatible.
	     Given two formulas $A$ and $B$ that do not have compatible models,
             we can conclude that $A$ does not entail $B$. We provide
	     two different abstractions (of different precision) of models.
	     Our algorithm is of interest wherever entailment checking
	     is performed (such as in program verifiers).},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-pays = {GB,NL},
  hal = {http://hal.inria.fr/hal-00777577}
}
@inproceedings{KanigFilliatre09wml,
  author = {Johannes Kanig and Jean-Christophe Filli\^atre},
  title = {{Who: A Verifier for Effectful Higher-order Programs}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  address = {Edinburgh, Scotland, UK},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  month = aug,
  year = 2009,
  url = {https://usr.lmf.cnrs.fr/~jcf/publis/wml09.pdf},
  hal = {http://hal.inria.fr/hal-00777585},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {ML},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  abstract = {We present Who, a tool for verifying effectful higher-order
  functions. It features {\em Effect polymorphism}, higher-order logic
  and the possibility to reason about state in the logic, which enable
  highly modular specifications of generic code. Several small
  examples and a larger case study demonstrate its usefulness. The
  Who~tool is intended to be used as an intermediate language for
  verification tools targeting ML-like programming languages.}
}
@inproceedings{MandelPlateauPouzet-MLworkshop-2009,
  author = {Louis Mandel and Florence Plateau and Marc Pouzet},
  title = {The {ReactiveML} Toplevel (Tool Demonstration)},
  booktitle = {ACM SIGPLAN Workshop on ML},
  address = {Edinburgh, Scotland, UK},
  topics = {team, lri},
  type_publi = {icolcomlec},
  month = aug,
  year = 2009,
  x-type = {article},
  x-support = {actes_aux},
  x-equipes = {demons PROVAL},
  x-cle-support = {ML},
  x-international-audience = {yes},
  x-proceedings = {no},
  x-editorial-board = {yes}
}
@inproceedings{LescuyerConchon09frocos,
  author = {St{\'e}phane Lescuyer and Sylvain Conchon},
  title = {Improving {Coq} Propositional Reasoning using a Lazy {CNF} Conversion Scheme},
  topics = {team},
  x-support = {actes},
  pages = {287-303},
  doi = {10.1007/978-3-642-04222-5_18},
  crossref = {frocos09}
}
@inproceedings{edmonson09arith,
  author = {William Edmonson and Guillaume Melquiond},
  title = {{IEEE} interval standard working group - {P1788}: current status},
  booktitle = {Proceedings of the 19th IEEE Symposium on Computer Arithmetic},
  editor = {Javier D. Bruguera and Marius Cornea and Debjit DasSarma and John Harrison},
  address = {Portland, OR, USA},
  year = {2009},
  pages = {231--234},
  doi = {10.1109/ARITH.2009.36},
  topics = {team},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-pays = {US},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  type_publi = {icolcomlec}
}
@inproceedings{Pouzet-lctes09,
  author = {Paul Caspi and Jean-Louis Cola\c{c}o and L\'eonard G\'erard
                  and Marc Pouzet and Pascal Raymond},
  title = {{Synchronous Objects with Scheduling Policies}:
                   Introducing safe shared memory in {Lustre}},
  year = {2009},
  month = jun,
  address = {Dublin},
  booktitle = {ACM International Conference on
                  Languages, Compilers, and Tools for Embedded Systems
                  (LCTES)},
  url-useless-since-prefix-missing = {lctes09.pdf},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-type = {article},
  x-support = {actes},
  topics = {team}
}
@inproceedings{Pouzet-emsoft09,
  author = {Marc Pouzet and Pascal Raymond},
  title = {Modular Static Scheduling of Synchronous Data-flow
                  Networks: An efficient symbolic representation},
  booktitle = {ACM International Conference on
                  Embedded Software (EMSOFT'09)},
  address = {Grenoble, France},
  month = {October},
  x-proceedings = {yes},
  x-international-audience = {yes},
  year = 2009,
  url-useless-since-prefix-missing = {emsoft09.pdf},
  x-type = {article},
  x-support = {actes},
  topics = {team}
}
@proceedings{jfla09,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2009,
  booktitle = {Vingti\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Saint-Quentin sur Is\`ere},
  publisher = {INRIA},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes}
}
@proceedings{frocos09,
  editor = {Silvio Ghilardi and
               Roberto Sebastiani},
  title = {Frontiers of Combining Systems, 7th International Symposium,
               FroCoS 2009, Proceedings},
  booktitle = {Frontiers of Combining Systems, 7th International Symposium, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5749},
  year = {2009},
  month = sep,
  address = {Trento, Italy},
  isbn = {978-3-642-04221-8},
  doi = {http://dx.doi.org/10.1007/978-3-642-04222-5},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes}
}