2013-conference.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc 2013-conference.cite -ob 2013-conference.bib -c 'year = 2013 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{Lelay13,
  hal = {http://hal.inria.fr/hal-00880212},
  author = {Catherine Lelay},
  title = {{A New Formalization of Power Series in Coq}},
  booktitle = {5th Coq Workshop},
  pages = {1--2},
  year = {2013},
  address = {Rennes, France},
  month = jul,
  note = {\url{http://coq.inria.fr/coq-workshop/2013#Lelay}},
  topics = {team}
}
@inproceedings{benzaken13popl,
  author = {V\'eronique Benzaken and Giuseppe Castagna and Kim Nguyen and J\'er\^ome Sim\'eon},
  title = {Static and Dynamic Semantics of {NoSQL} Languages},
  topics = {team},
  hal = {http://hal.archives-ouvertes.fr/hal-00797956},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  crossref = {popl13}
}
@inproceedings{marche13jfla,
  author = {Claude March\'e and Asma Tafat},
  title = {Calcul de plus faible pr\'econdition, revisité en {Why3}},
  crossref = {jfla13},
  topics = {team},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  hal = {http://hal.inria.fr/hal-00778791}
}
@inproceedings{conchon13jfla,
  author = {Sylvain Conchon and Alain Mebsout and Fatiha Za\"{\i}di},
  title = {V\'erification de syst\`emes param\'etr\'es avec {Cubicle}},
  crossref = {jfla13},
  topics = {team},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL Fortesse},
  x-type = {article},
  x-support = {actes},
  hal = {http://hal.inria.fr/hal-00778832}
}
@inproceedings{filliatre13jfla,
  author = {Jean-Christophe Filli\^atre and R\'emy El Siba\"{\i}e},
  title = {{Combine} : une biblioth\`eque {OCaml} pour la combinatoire},
  crossref = {jfla13},
  topics = {team},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL ext},
  x-type = {article},
  x-support = {actes},
  note = {\url{https://github.com/backtracking/combine/}},
  hal = {http://hal.inria.fr/hal-00779431},
  url = {http://hal.inria.fr/hal-00779431}
}
@inproceedings{mandel13jfla,
  author = {Louis Mandel and C{\'e}dric Pasteur},
  title = {R{\'e}activit{\'e} des syst{\`e}mes coop{\'e}ratifs : le cas de {ReactiveML}},
  crossref = {jfla13},
  topics = {team},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL ext},
  x-type = {article},
  x-support = {actes},
  note = {\url{http://rml.lri.fr/jfla13}},
  hal = {http://hal.inria.fr/hal-00779789},
  url = {http://www.lri.fr/~mandel/publications/MandelPasteur-JFLA-2013.pdf},
  abstract = {La concurrence coop{\'e}rative est un mod{\`e}le de programmation tr{\`e}s
r{\'e}pandu. On peut par exemple l'utiliser en OCaml {\`a} travers des
biblioth{\`e}ques comme Lwt, Async ou Equeue. Il a de nombreux avantages
tels que l'absence de courses critiques et des implantations l{\'e}g{\`e}res
et efficaces.  N{\'e}anmoins, un des inconv{\'e}nients majeurs de ce mod{\`e}le
est qu'il d{\'e}pend de la discipline du programmeur pour garantir que le
syst{\`e}me est r{\'e}actif : un processus peut emp{\^e}cher les autres de
s'ex{\'e}cuter.

ReactiveML est un langage qui {\'e}tend OCaml avec des constructions de
concurrence coop{\'e}rative. Il propose une analyse statique, l'analyse de
r{\'e}activit{\'e}, qui permet de d{\'e}tecter les expressions qui risquent de
produire des comportements non coop{\'e}ratifs.  Dans cet article, nous
pr{\'e}sentons cette analyse statique qui se d{\'e}finit {\`a} l'aide d'un syst{\`e}me
de types et effets.  Ainsi, comme le typage de donn{\'e}es aide les
programmeurs {\`a} d{\'e}tecter des erreurs d'ex{\'e}cution au plus t{\^o}t, l'analyse
de r{\'e}activit{\'e} aide {\`a} d{\'e}tecter des erreurs de concurrence.}
}
@inproceedings{BaudartJacquemardMandelPouzet-EMSOFT-2013,
  hal = {http://hal.inria.fr/hal-00850299},
  author = {Guillaume Baudart and Florent Jacquemard and Louis Mandel and Marc Pouzet},
  title = {A Synchronous Embedding of {Antescofo}, a Domain-Specific Language for Interactive Mixed Music},
  booktitle = {Thirteen International Conference on Embedded Software (EMSOFT'13)},
  year = 2013,
  month = sep,
  address = {Montreal, Canada},
  topics = {team},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL ext},
  x-type = {article},
  x-support = {actes},
  url = {http://reactiveml.org/publications/BaudartJacquemardMandelPouzet-EMSOFT-2013.pdf},
  webpage = {http://reactiveml.org/emsoft13},
  abstract = {Antescofo is recently developed software for \emph{musical score
  following} and \emph{mixed music}: it automatically, and in
real-time, synchronizes electronic instruments with a musician playing
on a classical instrument.  Therefore, it faces some of the same major
challenges as embedded systems.

The system provides a programming language used by composers to
specify musical pieces that mix interacting electronic and classical
instruments.  This language is developed with and for musicians and it
continues to evolve according to their needs.  Yet its semantics has
only recently been formally defined.  This paper presents a
\emph{synchronous semantics} for the core language of Antescofo and
an alternative implementation based on an embedding inside an
existing synchronous language, namely ReactiveML.
The semantics reduces to a few rules, is mathematically precise and
leads to an interpretor of only a few hundred lines. The efficiency of this
interpretor compares well with that of the actual implementation: on
all musical pieces we have tested, response times have been less than
the reaction time of the human ear.  Moreover, this embedding
permitted the prototyping of several new programming constructs, some
of which are described in this paper.}
}
@inproceedings{BaudartMandelPouzet-FARM-2013,
  hal = {http://hal.inria.fr/hal-00850294},
  author = {Guillaume Baudart and Louis Mandel and Marc Pouzet},
  title = {Programming Mixed Music in {ReactiveML}},
  booktitle = {ACM SIGPLAN Workshop on Functional Art, Music, Modeling and Design ({FARM'13})},
  year = 2013,
  month = sep,
  address = {Boston, USA},
  note = {Workshop ICFP 2013},
  url = {http://reactiveml.org/publications/BaudartMandelPouzet-FARM-2013.pdf},
  topics = {team},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL ext},
  x-type = {article},
  x-support = {actes},
  webpage = {http://reactiveml.org/farm13},
  abstract = {Mixed music is about live musicians interacting with electronic
  parts which are controlled by a computer during the performance.
  It allows composers to use and combine traditional instruments with
  complex synthesized sounds and other electronic devices.
  There are several languages dedicated to the writing of mixed music
  scores. Among them, the Antescofo language coupled with an
  advanced score follower allows a composer to manage the reactive
  aspects of musical performances: how electronic parts interact with
  a musician.
  However these domain specific languages do not offer the
  expressiveness of functional programming.

  We embed the Antescofo language in a reactive functional
  programming language, ReactiveML. This approach offers to the composer
  recursion, higher order, inductive types, as well as a
  simple way to program complex reactive behaviors thanks to the
  synchronous model of concurrency on which ReactiveML is built.
  This article presents how to program mixed music in ReactiveML through
  several examples.}
}
@inproceedings{MandelPasteurPouzet-PPDP-2013,
  hal = {http://hal.inria.fr/hal-00850290},
  author = {Louis Mandel and C{\'e}dric Pasteur and Marc Pouzet},
  title = {Time Refinement in a Functional Synchronous Language},
  booktitle = {Proceedings of 15th {ACM SIGPLAN} International Symposium on Principles and Practice of Declarative Programming ({PPDP'13})},
  year = 2013,
  address = {Madrid, Spain},
  month = sep,
  topics = {team},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL ext},
  x-type = {article},
  x-support = {actes},
  url = {http://reactiveml.org/publications/MandelPasteurPouzet-PPDP-2013.pdf},
  webpage = {http://reactiveml.org/ppdp13},
  abstract = {Concurrent and reactive systems often exhibit multiple time scales. For instance, in a discrete simulation, the scale at which agents communicate might be very different from the scale used to model the internals of each agent.

We propose an extension of the synchronous model of concurrency, called \emph{reactive domains}, to simplify the programming of such systems. Reactive domains allow the creation of local time scales and enable \emph{refinement}, that is, the replacement of an approximation of a system with a more detailed version without changing its behavior as observed by the rest of the program.

Our work is applied to the ReactiveML language, which extends ML with synchronous language constructs. We present an operational semantics for the extended language and a type system that ensures the soundness of programs.}
}
@inproceedings{paskevich13cade,
  hal = {http://hal.inria.fr/hal-00825086},
  author = {Jasmin C. Blanchette and Andrei Paskevich},
  title = {{TFF1}: The {TPTP} typed first-order form with rank-1 polymorphism},
  crossref = {cade13},
  x-equipes = {demons PROVAL},
  x-type = {article},
  topics = {team},
  url = {http://www4.in.tum.de/~blanchet/tff1short.pdf}
}
@inproceedings{boldo13arith,
  author = {Sylvie Boldo},
  title = {How to Compute the Area of a Triangle: a Formal Revisit},
  booktitle = {Proceedings of the 21th IEEE Symposium on Computer Arithmetic},
  address = {Austin, Texas, USA},
  year = {2013},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ARITH},
  x-international-audience = {yes},
  x-proceedings = {yes},
  hal = {http://hal.inria.fr/hal-00790071}
}
@inproceedings{bolmel13arith,
  author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond, Guillaume},
  title = {A Formally-Verified {C} Compiler Supporting Floating-Point Arithmetic},
  booktitle = {Proceedings of the 21th IEEE Symposium on Computer Arithmetic},
  address = {Austin, Texas, USA},
  year = {2013},
  topics = {team},
  x-equipes = {demons PROVAL ext},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ARITH},
  x-international-audience = {yes},
  x-proceedings = {yes},
  hal = {http://hal.inria.fr/hal-00743090}
}
@inproceedings{filliatre13esop,
  author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
  title = {Why3 --- Where Programs Meet Provers},
  booktitle = {Proceedings of the 22nd European Symposium on Programming},
  month = mar,
  year = 2013,
  volume = {7792},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Matthias Felleisen and Philippa Gardner},
  pages = {125--128},
  hal = {http://hal.inria.fr/hal-00789533},
  topics = {team,lri},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ESOP},
  x-editorial-board = {yes},
  x-international-audience = {yes}
}
@inproceedings{chargueraud13esop,
  author = {Arthur Chargu{\'e}raud},
  title = {Pretty-Big-Step Semantics},
  booktitle = {Proceedings of the 22nd European Symposium on Programming},
  month = mar,
  year = 2013,
  volume = {7792},
  editor = {Matthias Felleisen and Philippa Gardner},
  pages = {41--60},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  hal = {http://hal.inria.fr/hal-00798227},
  topics = {team,lri},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ESOP},
  x-editorial-board = {yes},
  x-international-audience = {yes}
}
@inproceedings{chargueraud13ppopp,
  author = {Umut A. Acar and Arthur Chargu{\'e}raud and Mike Rainey},
  title = {Scheduling parallel programs by work stealing with private deques},
  booktitle = {Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of parallel programming},
  month = feb,
  year = 2013,
  series = {PPoPP '13},
  pages = {219-228},
  publisher = {ACM Press},
  doi = {10.1145/2442516.2442538},
  hal = {http://hal.inria.fr/hal-00863028},
  topics = {team,lri},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {PPOPP},
  x-editorial-board = {yes},
  x-international-audience = {yes}
}
@inproceedings{filliatre13plmw,
  author = {Jean-Christophe Filli\^atre},
  title = {{Deductive Program Verification}},
  booktitle = {{Programming Languages Mentoring Workshop (PLMW 2013)}},
  editor = {Nate Foster and Philippa Gardner and Alan Schmitt and
 Gareth Smith and Peter Thieman and Tobias Wrigstad},
  month = {January},
  hal = {http://hal.inria.fr/hal-00799190},
  year = 2013,
  topics = {team},
  type_digiteo = {conf_autre},
  type_publi = {colloque},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {no},
  x-invited-conference = {yes},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-support = {actes},
  address = {Rome, Italy}
}
@inproceedings{filliatre13cade,
  author = {Jean-Christophe Filli\^atre},
  title = {One Logic To Use Them All},
  crossref = {cade13},
  pages = {1--20},
  topics = {team,lri},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-invited-conference = {yes},
  hal = {http://hal.inria.fr/hal-00809651/en/}
}
@inproceedings{bobot13vstte,
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
  hal = {http://hal.inria.fr/hal-00875395},
  title = {Preserving User Proofs Across Specification Changes},
  crossref = {vstte13},
  pages = {191--201},
  topics = {team,lri},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{IshMelNak13,
  hal = {http://hal.inria.fr/hal-00806701},
  author = {Daisuke Ishii and Guillaume Melquiond and Shin Nakajima},
  title = {Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus},
  booktitle = {Proceedings of the 10th Conference on Integrated Formal Methods},
  editor = {Einar Broch Johnsen and Luigia Petre},
  address = {Turku, Finland},
  year = {2013},
  pages = {139--153},
  series = {Lecture Notes in Computer Science},
  volume = {7940},
  doi = {10.1007/978-3-642-38613-8_10},
  topics = {team,lri},
  type_publi = {icolcomlec}
}
@inproceedings{conchon13fmcad,
  topics = {team},
  hal = {http://hal.archives-ouvertes.fr/hal-00924640},
  title = {Invariants for Finite Instances and Beyond},
  author = {Conchon, Sylvain and Goel, Amit and Krsti{\'c}, Sava and Mebsout, Alain and Za{\"\i}di, Fatiha},
  abstract = {Verification of safety properties of concurrent programs with an arbitrary numbers of processes is an old challenge. In particular, complex parameterized protocols like FLASH are still out of the scope of state-of-the-art model checkers. In this paper, we describe a new algorithm, called Brab, that is able to automatically infer invariants strong enough to prove a protocol like FLASH. Brab computes over-approximations of backward reachable states that are checked to be unreachable in a finite instance of the system. These approximations (candidate invariants) are then model checked together with the original safety properties. Completeness of the approach is ensured by a mechanism for backtracking on spurious traces introduced by too coarse approximations.},
  booktitle = {FMCAD},
  pages = {61--68},
  address = {Portland, Oregon, {\'E}tats-Unis},
  audience = {internationale},
  doi = {10.1109/FMCAD.2013.6679392},
  year = 2013,
  month = oct
}
@inproceedings{conchon13synasc,
  topics = {team},
  author = {Conchon, Sylvain and Iguernelala, Mohamed and Mebsout, Alain},
  title = {A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo},
  year = 2013,
  doi = {10.1109/SYNASC.2013.29},
  booktitle = {15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing},
  pages = {161--168}
}
@inproceedings{filliatre13msr,
  author = {Jean-Christophe Filli\^atre},
  title = {Deductive Program Verification with {Why3}},
  booktitle = {MSR-Inria Joint Centre ``Spring Day''},
  year = 2013,
  month = may,
  address = {Lyon, France},
  note = {Invited talk},
  topics = {team, lri},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-invited-conference = {yes},
  x-international-audience = {yes}
}
@proceedings{popl13,
  title = {Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year = 2013,
  booktitle = {Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  editor = {R. Cousot},
  address = {Roma, Italy},
  month = jan,
  publisher = {ACM Press}
}
@proceedings{jfla13,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2013,
  booktitle = {Vingt-quatri\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = feb,
  address = {Aussois, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@proceedings{cade13,
  title = {24th International Conference on Automated Deduction},
  booktitle = {24th International Conference on Automated Deduction (CADE-24)},
  address = {Lake Placid, USA},
  month = {June},
  year = 2013,
  series = {Lecture Notes in Artificial Intelligence},
  volume = 7898,
  publisher = {Springer}
}
@proceedings{vstte13,
  booktitle = {Verified Software: Theories, Tools, Experiments (5th International Conference VSTTE)},
  month = may,
  year = 2013,
  address = {Atherton, USA},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {VSTTE},
  editor = {Ernie Cohen and Andrey Rybalchenko},
  series = {Lecture Notes in Computer Science},
  volume = {8164},
  publisher = {Springer}
}