2009-conference.bib
@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: 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}
}