complete-conference.bib

@comment{{This file has been generated by bib2bib 1.97pl2}}
@comment{{Command line: bib2bib -oc complete-conference.cite -ob complete-conference.bib -c 'topics : "team" and $type="inproceedings" and year>=2004' /users/demons/filliatr/bibliodemons/abbrevs.bib /users/demons/filliatr/bibliodemons/demons.bib /users/demons/filliatr/bibliodemons/demons2.bib /users/demons/filliatr/bibliodemons/demons3.bib /users/demons/filliatr/bibliodemons/team.bib /users/demons/filliatr/bibliodemons/crossrefs.bib}}
@inproceedings{castagna08icfp,
  author = {Giuseppe Castagna and Kim Nguyen},
  title = {Typed iterators for {XML}},
  booktitle = {ICFP},
  year = {2008},
  pages = {15--26},
  ee = {http://doi.acm.org/10.1145/1411204.1411210},
  crossref = {icfp08},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  topics = {team}
}
@inproceedings{jacobs04amast,
  author = {Bart Jacobs and Claude March{\'e} and Nicole Rauch},
  title = {Formal Verification of a Commercial Smart Card Applet with
  Multiple Tools},
  crossref = {amast04},
  year = 2004,
  topics = {team}
}
@inproceedings{barthe05fast,
  author = {G. Barthe and T. Rezk and A. Saabas},
  title = {{Proof obligations preserving compilation}},
  year = 2005,
  crossref = {fast05},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Tamara.Rezk//publication/Barthe-Rezk-Saabas.pdf},
  pages = {112-126},
  topics = {team}
}
@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},
  pages = {45-59},
  doi = {http://dx.doi.org/10.1007/978-3-642-19835-9_6},
  abstract = {http://www.lri.fr/~contejea/publis/2011tacas/abstract.html}
}
@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{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},
  crossref = {icde11}
}
@inproceedings{andronick05,
  author = {June Andronick and Boutheina Chetali and Paulin-Mohring, Christine},
  title = {Formal Verification of Security Properties of Smart Card Embedded Source Code},
  topics = {team},
  x-pdf = {http://jandronick.free.fr/publi/FM2005.pdf},
  url = {http://jandronick.free.fr/publi/FM2005.pdf},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {FME},
  crossref = {fm05}
}
@inproceedings{andronick06,
  author = {June Andronick and Boutheina Chetali},
  title = {{An Environment for Securing Smart
                Cards Embedded C Code}},
  year = {2006},
  booktitle = {{International Conference on Research in
                 Smart Cards (Esmart'06)}},
  x-pdf = {http://jandronick.free.fr/publi/ESMART2006.pdf},
  url = {http://jandronick.free.fr/publi/ESMART2006.pdf},
  topics = {team},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes}
}
@inproceedings{audebaud06mpc,
  author = {Philippe Audebaud and Christine Paulin-Mohring},
  title = {Proofs of Randomized Algorithms in {Coq}},
  crossref = {mpc2006},
  x-equipes = {demons PROVAL EXT},
  x-pdf = {http://www.lri.fr/~paulin/ALEA/article.pdf},
  url = {http://www.lri.fr/~paulin/ALEA/article.pdf},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {MPC},
  topics = {team},
  type_publi = {icolcomlec},
  year = 2006
}
@inproceedings{Biernacka07wrs,
  author = {Malgorzata Biernacka and Dariusz Biernacki},
  title = {{Formalizing Constructions of Abstract Machines for Functional Languages in {Coq}}},
  booktitle = {{7th International Workshop on Reduction
Strategies in Rewriting and Programming (WRS 2007)}},
  year = 2007,
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  address = {Paris, France},
  month = {June},
  pages = {84--99},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-pdf = {http://www.lsv.ens-cachan.fr/rdp07/WRSproceedings.pdf},
  url = {http://www.lsv.ens-cachan.fr/rdp07/WRSproceedings.pdf},
  topics = {team, lri}
}
@inproceedings{Biernacki07apges,
  author = {Dariusz Biernacki and Jean-Louis Cola\c{c}o and Marc Pouzet},
  title = {{Clock-directed Modular Code Generation from Synchronous Block Diagrams}},
  booktitle = {{Workshop on Automatic Program Generation for Embedded
Systems (APGES 2007)}},
  year = 2007,
  address = {Salzburg, Austria},
  month = {October},
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes_aux},
  x-pdf = {http://www-fp.dcs.st-and.ac.uk/APGES/OnlineProceedings/11-Pouzet.pdf},
  url = {http://www-fp.dcs.st-and.ac.uk/APGES/OnlineProceedings/11-Pouzet.pdf},
  topics = {team, lri}
}
@inproceedings{Bol06,
  author = {Sylvie Boldo},
  title = {Pitfalls of a full floating-point proof: example on the formal proof of the {Veltkamp/Dekker} algorithms},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  pages = {52-66},
  x-pdf = {http://www.lri.fr/~sboldo/files/ijcar06.pdf},
  url = {http://www.lri.fr/~sboldo/files/ijcar06.pdf},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {IJCAR},
  crossref = {ijcar06}
}
@inproceedings{BolMun06,
  author = {Sylvie Boldo and C\'esar Mu{\~n}oz},
  title = {Provably Faithful Evaluation of Polynomials},
  booktitle = {Proceedings of the 21st Annual ACM Symposium on Applied Computing},
  year = {2006},
  month = apr,
  address = {Dijon, France},
  topics = {team},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  volume = 2,
  hal = {http://hal.inria.fr/inria-00050232/en/},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {SAC},
  pages = {1328-1332}
}
@inproceedings{BoldoFilliatre07,
  author = {Sylvie Boldo and Jean-Christophe Filli\^atre},
  title = {{Formal Verification of Floating-Point Programs}},
  booktitle = {18th IEEE International Symposium on Computer Arithmetic},
  pages = {187-194},
  month = {June},
  year = 2007,
  address = {Montpellier, France},
  topics = {team,lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ARITH},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf},
  abstract = {
  This paper introduces a methodology to perform formal verification
  of floating-point C programs. It extends an existing tool for the
  verification of C programs, Caduceus, with new annotations specific
  to floating-point arithmetic. The Caduceus first-order logic model
  for C programs is extended accordingly. Then verification conditions
  expressing the correctness of the programs are obtained in the usual
  way and can be discharged interactively with the Coq proof
  assistant, using an existing Coq formalization of floating-point
  arithmetic.  This methodology is already implemented and has been
  successfully applied to several short floating-point programs, which
  are presented in this paper.}
}
@inproceedings{conchon05jfla,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre and Julien Signoles},
  title = {Le foncteur sonne toujours deux fois},
  topics = {team, lri},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  crossref = {jfla05},
  pages = {79--94},
  url = {http://www.lri.fr/~filliatr/ftp/publis/jfla05.ps.gz}
}
@inproceedings{conchon07afm,
  author = {Sylvain Conchon and \'Evelyne Contejean and Johannes Kanig and St{\'e}phane Lescuyer},
  title = {{Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant}},
  crossref = {afm07},
  abstract = {Ergo is a little engine of proof dedicated to program
  verification. It fully supports quantifiers and directly handles
  polymorphic sorts. Its core component is CC(X), a new combination
  scheme for the theory of uninterpreted symbols parameterized by a
  built-in theory X. In order to make a sound integration in a proof
  assistant possible, Ergo is capable of generating proof traces
  for CC(X).  Alternatively, Ergo can also be called interactively
  as a simple oracle without further verification. It is currently
  used to prove correctness of C and Java programs as part of the Why
  platform.},
  abstract = {http://www.lri.fr/~contejea/publis/2007afm/abstract.html},
  topics = {team,lri},
  type_digiteo = {conf_isbn},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {AFM},
  x-pdf = {http://fm.csl.sri.com/AFM07/afm07-preprint.pdf},
  url = {http://fm.csl.sri.com/AFM07/afm07-preprint.pdf},
  doi = {http://dx.doi.org/10.1145/1345169.1345176},
  pages = {55--59}
}
@inproceedings{conchon07smt,
  author = {Sylvain Conchon and \'Evelyne Contejean and Johannes Kanig},
  title = {{CC(X)}: Efficiently Combining Equality and Solvable Theories without Canonizers},
  booktitle = {SMT 2007: 5th International Workshop on Satisfiability Modulo},
  year = 2007,
  editor = {Sava Krstic and Albert Oliveras},
  topics = {team,lri},
  type_digiteo = {conf_autre},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {SMT}
}
@inproceedings{conchon08smt,
  author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean
  and St\'ephane Lescuyer},
  title = {{Implementing Polymorphism in SMT solvers}},
  booktitle = {SMT 2008: 6th International Workshop on Satisfiability Modulo},
  pages = {1--5},
  year = 2008,
  editor = {Clark Barrett and Leonardo de Moura},
  volume = 367,
  series = {ACM International Conference Proceedings Series},
  topics = {team,lri},
  type_digiteo = {conf_autre},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {SMT},
  x-pdf = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
  url = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  isbn = {978-1-60558-440-9},
  doi = {http://dx.doi.org/10.1145/1512464.1512466},
  abstract = {http://www.lri.fr/~contejea/publis/2008smt/abstract.html}
}
@inproceedings{conchon07tfp,
  author = {Sylvain Conchon and
     Jean-Christophe Filli\^atre and
     Julien Signoles},
  title = {{Designing a Generic Graph Library using {ML} Functors}},
  booktitle = {The Eighth Symposium on Trends in Functional Programming},
  editor = {Marco T. Moraz\'an and Henrik Nilsson},
  publisher = {Seton Hall University},
  volume = {TR-SHU-CS-2007-04-1},
  pages = {XII/1--13},
  year = 2007,
  address = {New York, USA},
  month = apr,
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  abstract = {
  This paper details the design and implementation of Ocamlgraph, a
  highly generic graph library for the programming language Ocaml.
  This library features a large set of graph data
  structures---directed or undirected, with or without labels on
  vertices and edges, as persistent or mutable data structures,
  etc.---and a large set of graph algorithms.  Algorithms are written
  independently from graph data structures, which allows combining
  user data structure (resp. algorithm) with Ocamlgraph algorithm
  (resp. data structure).  Genericity is obtained through massive use
  of the Ocaml module system and its functions, the so-called
  functors.},
  url = {http://www.lri.fr/~filliatr/ftp/publis/ocamlgraph-tfp07.ps},
  topics = {team, lri},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-editorial-board = {yes}
}
@inproceedings{conchon08tfp,
  author = {Sylvain Conchon and
     Jean-Christophe Filli\^atre and
     Julien Signoles},
  title = {Designing a Generic Graph Library using {ML} Functors},
  booktitle = {Trends in Functional Programming (TFP'07)},
  month = {April},
  year = 2007,
  address = {New York City, USA},
  topics = {team, lri},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {TFP},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/ocamlgraph-tfp-8.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/ocamlgraph-tfp-8.pdf},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{conchon08entcs,
  author = {Sylvain Conchon and \'Evelyne Contejean and Johannes Kanig and St\'ephane Lescuyer},
  title = {{CC(X)}: Semantical Combination of Congruence Closure with
    Solvable Theories},
  booktitle = {Post-proceedings of the 5th International Workshop on
                  Satisfiability Modulo Theories ({SMT 2007})},
  series = {Electronic Notes in Computer Science},
  publisher = {Elsevier Science Publishers},
  volume = {198(2)},
  pages = {51--69},
  year = 2008,
  abstract = {
  We present a generic congruence closure algorithm for deciding
  ground formulas in the combination of the theory of equality with
  uninterpreted symbols and an arbitrary built-in solvable theory X.
  Our algorithm CC(X) is reminiscent of Shostak combination: it
  maintains a union-find data-structure modulo X from which maximal
  information about implied equalities can be directly used for
  congruence closure.  CC(X) diverges from Shostak's approach by the use
  of semantical values for class representatives instead of canonized
  terms. Using semantical values truly reflects the actual
  implementation of the decision procedure for X.  It also enforces to
  entirely rebuild the algorithm since global canonization, which is
  at the heart of Shostak combination, is no longer feasible with
  semantical values.  CC(X) has been implemented in Ocaml and is at
  the core of Ergo, a new automated theorem prover dedicated to
  program verification.
},
  abstract = {http://www.lri.fr/~contejea/publis/2008entcs/abstract.html},
  topics = {team},
  type_publi = {irevcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {ENTCS},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  doi = {http://dx.doi.org/10.1016/j.entcs.2008.04.080}
}
@inproceedings{Conchon08jfla,
  author = {Sylvain Conchon and Johannes Kanig and St\'ephane Lescuyer},
  title = {{SAT-MICRO : petit mais costaud !}},
  year = 2008,
  topics = {team, lri},
  type_publi = {colcomlec},
  type_digiteo = {conf_autre},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  x-editorial-board = {yes},
  x-international-audience = {no},
  x-proceedings = {yes},
  crossref = {jfla08},
  address = {\'Etretat, France},
  publisher = {INRIA},
  url = {http://www.lri.fr/~conchon/publis/conchon-jfla08.ps},
  abstract = {
  Le probl\`eme SAT, qui consiste `a d\'eterminer si une formule bool\'eenne
  est satisfaisable, est un des probl\`emes NP-complets les plus
  c\'el\`ebres et aussi un des plus \'etudi\'es. Bas\'es initialement sur la
  proc\'edure DPLL, les SAT-solvers modernes ont connu des
  progr\`es spectaculaires ces dix derni\`eres ann\'ees dans leurs
  performances, essentiellement gr\^ace \`a deux optimisations: le retour
  en arri\`ere non-chronologique et l'apprentissage par analyse des
  clauses conflits. Nous proposons dans cet article une \'etude formelle
  du fonctionnement de ces techniques ainsi qu'une r\'ealisation en Ocaml
  d'un SAT-solver, baptis\'e SAT-MICRO, int\'egrant ces
  optimisations. Le fonctionnement de SAT-MICRO est d\'ecrit par un
  ensemble de r\`egles d'inf\'erence et la taille de son code, 70 lignes
  au total, permet d'envisager sa certification compl\`ete.}
}
@inproceedings{ConchonFilliatre06wml,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Type-Safe Modular Hash-Consing}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  address = {Portland, Oregon},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  month = sep,
  year = 2006,
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {ML}
}
@inproceedings{ConchonFilliatre07jfla,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Union-Find Persistant}},
  year = 2007,
  topics = {team, lri},
  type_publi = {colcomlec},
  type_digiteo = {conf_autre},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  crossref = {jfla07},
  pages = {135--149},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/puf.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/puf.pdf},
  abstract = {
  Le probl\`eme des classes disjointes, connu sous le nom de
  \emph{union-find}, consiste \`a maintenir dans une structure de
  donn\'ees une partition d'un ensemble fini. Cette structure fournit deux
  op\'erations : une fonction \emph{find} d\'eterminant la classe d'un
  \'el\'ement et une fonction \emph{union} r\'eunissant deux classes.  Une
  solution optimale et imp\'erative, due \`a Tarjan, est connue depuis
  longtemps.

  Cependant, le caract\`ere imp\'eratif de cette structure de donn\'ees
  devient g\^enant lorsqu'elle est utilis\'ee dans un contexte o\`u
  s'effectuent des retours en arri\`ere (\emph{backtracking}). Nous
  pr\'esentons dans cet article une version persistante de
  \emph{union-find} dont la complexit\'e est comparable \`a celle de la
  solution imp\'erative. Pour obtenir cette efficacit\'e, notre solution
  utilise massivement des traits imp\'eratifs. C'est pourquoi nous
  pr\'esentons \'egalement une preuve formelle de correction, pour
  s'assurer notamment du caract\`ere persistant de cette solution.
}
}
@inproceedings{ConchonFilliatre07wml,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{A Persistent Union-Find Data Structure}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  publisher = {ACM},
  pages = {37--45},
  year = 2007,
  address = {Freiburg, Germany},
  month = {October},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf},
  abstract = { The problem of disjoint sets, also known as union-find,
  consists in maintaining a partition of a finite set within a data
  structure. This structure provides two operations: a function find
  returning the class of an element and a function union merging two
  classes. An optimal and imperative solution is known since 1975.
  However, the imperative nature of this data structure may be a
  drawback when it is used in a backtracking algorithm. This paper
  details the implementation of a persistent union-find data structure
  as efficient as its imperative counterpart.  To achieve this result,
  our solution makes heavy use of imperative features and thus it is a
  significant example of a data structure whose side effects are
  safely hidden behind a persistent interface.  To strengthen this
  last claim, we also detail a formalization using the Coq proof
  assistant which shows both the correctness of our solution and its
  observational persistence. },
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {ML}
}
@inproceedings{Filliatre08wml,
  author = {Jean-Christophe Filli\^atre},
  title = {{A Functional Implementation of the Garsia--Wachs Algorithm}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  publisher = {ACM},
  year = 2008,
  address = {Victoria, British Columbia, Canada},
  month = {September},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-pdf = {http://www.lri.fr/~filliatr/publis/gw-wml08.pdf},
  url = {http://www.lri.fr/~filliatr/publis/gw-wml08.pdf},
  abstract = {  This functional pearl proposes an ML implementation of
  the Garsia--Wachs algorithm.
  This somewhat obscure algorithm builds a binary tree with minimum
  weighted path length from weighted leaf nodes given in symmetric
  order. Our solution exhibits the usual benefits of functional
  programming (use of immutable data structures, pattern-matching,
  polymorphism) and nicely compares to the purely imperative
  implementation from \emph{The Art of Computer Programming}.},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {ML}
}
@inproceedings{ConchonFilliatre08esop,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Semi-Persistent Data Structures}},
  crossref = {esop08},
  year = 2008,
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/spds-rr.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/spds-rr.pdf},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ESOP},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{contejean04rta,
  author = {\'Evelyne Contejean},
  title = {{A certified AC matching algorithm}},
  booktitle = {15th International Conference on Rewriting Techniques and Applications},
  crossref = {rta04},
  pages = {70--84},
  year = 2004,
  type_publi = {icolcomlec},
  topics = {team},
  doi = {http://dx.doi.org/10.1007/978-3-540-25979-4_5},
  abstract = {http://www.lri.fr/~contejea/publis/2004rta/abstract.html}
}
@inproceedings{contejean05cade,
  author = {\'Evelyne Contejean and Pierre Corbineau},
  title = {Reflecting Proofs in First-Order Logic with Equality},
  type_publi = {icolcomlec},
  topics = {team},
  pages = {7--22},
  crossref = {cade05},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CADE},
  abstract = {http://www.lri.fr/~contejea/publis/2005cade/abstract.html},
  doi = {http://dx.doi.org/10.1007/11532231_2}
}
@inproceedings{contejean07frocos,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
  title = {Certification of automated termination proofs},
  crossref = {frocos07},
  pages = {148--162},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {FROCOS},
  topics = {team},
  doi = {http://dx.doi.org/10.1007/978-3-540-74621-8_10},
  abstract = {http://www.lri.fr/~contejea/publis/2007frocos/abstract.html}
}
@inproceedings{contejean08wsct,
  author = {\'Evelyne Contejean and Xavier Urbain},
  title = {{The A3PAT approach}},
  booktitle = { Workshop on Certified Termination WScT08},
  year = 2008,
  address = {Leipzig, Germany},
  month = may,
  topics = {team},
  x-international-audience = {yes},
  x-proceedings = {no}
}
@inproceedings{contejean08types,
  author = {\'Evelyne Contejean},
  title = {{Coccinelle, a Coq library for rewriting}},
  booktitle = {Types},
  year = 2008,
  address = {Torino, Italy},
  month = mar,
  type_publi = {autre},
  x-equipes = {demons PROVAL},
  topics = {team},
  x-international-audience = {yes},
  x-proceedings = {no}
}
@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 = {http://doi.acm.org/10.1145/1706356.1706370},
  abstract = {http://www.lri.fr/~contejea/publis/2010pepm/abstract.html}
}
@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},
  urn = {urn:nbn:de:0030-drops-31192},
  doi = {http://dx.doi.org/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{corbineau04,
  author = {Pierre Corbineau},
  title = {First-order reasoning in the {Calculus of Inductive Constructions}},
  crossref = {types03},
  booktitle = {TYPES 2003 : Types for Proofs and Programs},
  pages = {162--177},
  year = 2004,
  editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
  volume = 3085,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  topics = {team},
  type_publi = {icolcomlec},
  ps = {http://www.lri.fr/~corbinea/ftp/publis/types03.ps},
  url = {http://www.lri.fr/~corbinea/ftp/publis/types03.ps}
}
@inproceedings{corbineau05jfla,
  author = {Pierre Corbineau},
  title = {Skip lists et arbres binaires de recherche probabilistes},
  topics = {team,colcomlec},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  crossref = {jfla05},
  pages = {99--112}
}
@inproceedings{couchot07ftp,
  author = {Jean-Fran\c{c}ois Couchot and Thierry Hubert},
  title = {{A Graph-based Strategy for the Selection of Hypotheses}},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {FTP},
  booktitle = {FTP 2007 - International Workshop on
                   First-Order Theorem Proving},
  address = {Liverpool, UK},
  month = sep,
  year = 2007,
  pages = {},
  x-pdf = {http://www.lri.fr/~couchot/IMG/pdf_couchot_hubert.pdf},
  url = {http://www.lri.fr/~couchot/IMG/pdf_couchot_hubert.pdf},
  abstract = {In previous works on verifying
C programs by deductive approaches based on SMT provers,
we proposed the heuristic of separation analysis to handle the most
difficult problems.
Nevertheless, this heuristic is not sufficient when applied on
industrial C programs:
it remains some Verification  Conditions (VCs) that cannot be decided
by any SMT prover, mainly due to their size.
This work presents a strategy to select relevant hypotheses
in each VC.
The relevance of an hypothesis is the combination of
two separated dependency analysis
obtained by some graph traversals.
The approach is applied on a benchmark issued from
an industrial program verification.
}
}
@inproceedings{couchot07cade,
  author = {Jean-Fran\c{c}ois Couchot and St\'ephane Lescuyer},
  title = {Handling Polymorphism in Automated Deduction},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CADE},
  pages = {263--278},
  booktitle = {21th International Conference on Automated Deduction (CADE-21)},
  address = {Bremen, Germany},
  month = jul,
  year = 2007,
  series = {LNCS (LNAI)},
  volume = 4603,
  x-pdf = {http://www.lri.fr/~couchot/IMG/pdf_CADE_couchot_lescuyer.pdf},
  url = {http://www.lri.fr/~couchot/IMG/pdf_CADE_couchot_lescuyer.pdf},
  abstract = {Polymorphism has become a common way of designing short and reusable
programs by abstracting generic definitions from type-specific ones.
Such a convenience is valuable in logic as well, because it unburdens
the specifier from writing redundant declarations of logical
symbols.
However,
top shelf automated theorem provers  such as
Simplify, Yices or other SMT-LIB ones do not handle polymorphism. To
this end, we present
efficient reductions of polymorphism in both unsorted and many-sorted
first order logics.
For each encoding, we show that the formulas and their encoded
counterparts are logically equivalent in the context of automated
theorem proving. The efficiency keynote is to disturb the prover as
little as possible, especially the internal decision procedures used for
special sorts, e.g. integer linear arithmetic, to which we apply a
special treatment.
The corresponding implementations are presented in the framework of
the Why/Caduceus
toolkit.}
}
@inproceedings{CouchotD07IFM,
  author = {Jean-Fran\c{c}ois Couchot and
               Fr\'ed\'eric Dadeau},
  title = {Guiding the Correction of Parameterized Specifications},
  booktitle = {Integrated Formal Methods},
  publisher = {Springer},
  address = {Oxford, UK},
  month = jul,
  topics = {team, lri},
  series = {Lecture Notes in Computer Science},
  volume = 4591,
  pages = {176--194},
  year = 2007,
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {IFM},
  x-pdf = {http://www.lri.fr/~couchot/IMG/pdf/CD07.pdf},
  url = {http://www.lri.fr/~couchot/IMG/pdf/CD07.pdf},
  abstract = {
Finding inductive invariants is a key issue in many domains such as
program verification, model based testing, etc.
However, few approaches help the designer in the task of writing
a correct and meaningful model, where  correction is used for
consistency of the formal specification  w.r.t. its inner invariant
properties.
Meaningfulness is obtained by providing many explicit views of the model,
like animation, counter-example extraction, and so on.
We propose to ease the task of writing a correct and meaningful formal
specification
by combining a panel of provers,
a set-theoretical constraint
solver and some model-checkers.}
}
@inproceedings{duran04pepm,
  author = {Francisco Dur{\'a}n and Salvador Lucas and Jos{\'e} Meseguer
and Claude March{\'e} and Xavier  Urbain},
  title = {Proving Termination of Membership Equational Programs},
  crossref = {pepm04},
  topics = {team},
  type_publi = {icolcomlec}
}
@inproceedings{filliatre04icfem,
  author = {Jean-Christophe Filli{\^a}tre and Claude March{\'e}},
  title = {Multi-Prover Verification of {C} Programs},
  crossref = {icfem04},
  year = {2004},
  pages = {15--29},
  topics = {team},
  type_publi = {icolcomlec},
  url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus.ps.gz}
}
@inproceedings{filliatre06jfla,
  author = {Jean-Christophe Filli\^atre},
  title = {It\'erer avec persistance},
  topics = {team, lri},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  crossref = {jfla06},
  url = {http://www.lri.fr/~filliatr/ftp/publis/enum.ps.gz}
}
@inproceedings{filliatre07cav,
  author = {Jean-Christophe Filli\^atre and Claude March\'e},
  title = {The {Why/Krakatoa/Caduceus} Platform for Deductive Program
  Verification},
  crossref = {cav07},
  pages = {173--177},
  topics = {team, lri},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf},
  x-equipes = {demons PROVAL EXT},
  x-type = {articlecourt},
  x-support = {actes},
  x-cle-support = {CAV}
}
@inproceedings{Filliatre06wml,
  author = {Jean-Christophe Filli\^atre},
  title = {{Backtracking iterators}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  address = {Portland, Oregon},
  month = sep,
  year = 2006,
  topics = {team, lri},
  type_publi = {icolcomlec},
  x-pdf = {http://www.lri.fr/~filliatr/publis/enum2.pdf},
  url = {http://www.lri.fr/~filliatr/publis/enum2.pdf},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {ML}
}
@inproceedings{Filliatre07corde,
  author = {Jean-Christophe Filli\^atre},
  title = {{Gagner en passant \`a la corde}},
  year = 2008,
  topics = {team, lri},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  x-editorial-board = {yes},
  x-international-audience = {no},
  x-proceedings = {yes},
  crossref = {jfla08},
  address = {\'Etretat, France},
  publisher = {INRIA},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/cordes.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/cordes.pdf},
  abstract = {
  Cet article pr\'esente une r\'ealisation en Ocaml de la structure de
  cordes introduite par Boehm, Atkinson et Plass. Nous montrons
  notamment comment cette structure de donn\'ees s'\'ecrit naturellement
  comme un foncteur, transformant une structure de s\'equence en une
  autre structure de m\^eme interface. Cette fonctorisation a de
  nombreuses applications au-del\`a de l'article original. Nous en
  donnons plusieurs, dont un \'editeur de texte dont les performances
  sur de tr\`es gros fichiers sont bien meilleures que celles des
  \'editeurs les plus populaires.}
}
@inproceedings{Filliatre07mix,
  author = {Jean-Christophe Filli\^atre},
  title = {{Formal Verification of MIX Programs}},
  booktitle = {{Journ{\'e}es en l'honneur de Donald E. Knuth}},
  year = 2007,
  note = {\url{http://knuth07.labri.fr/exposes.php}},
  address = {Bordeaux, France},
  month = {October},
  topics = {team, lri},
  type_publi = {colcomlec},
  type_digiteo = {conf_autre},
  x-pdf = {http://www.lri.fr/~filliatr/publis/verifmix.pdf},
  url = {http://www.lri.fr/~filliatr/publis/verifmix.pdf},
  abstract = {We introduce a methodology to formally verify MIX programs.
  It consists in annotating a MIX program with logical annotations
  and then to turn it into a set of purely sequential programs on
  which classical techniques can be applied.
  Contrary to other approaches of verification of unstructured
  programs, we do not impose the location of annotations but only the
  existence of at least one invariant on each cycle in the control
  flow graph. A prototype has been implemented and used to verify
  several programs from \emph{The Art of Computer Programming}.},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux}
}
@inproceedings{FilliatreLetouzey04esop,
  author = {Jean-Christophe Filli\^atre and Pierre Letouzey},
  title = {{Functors for Proofs and Programs}},
  booktitle = {Proceedings of The European Symposium on Programming},
  year = 2004,
  address = {Barcelona, Spain},
  month = apr,
  series = {Lecture Notes in Computer Science},
  volume = 2986,
  pages = {370--384},
  topics = {team},
  type_publi = {icolcomlec},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/fpp.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/fpp.pdf}
}
@inproceedings{hubert05sefm,
  author = {Thierry Hubert and Claude March\'e},
  topics = {team},
  title = {A case study of {C} source code verification: the {Schorr-Waite} algorithm},
  crossref = {sefm05},
  type_publi = {icolcomlec},
  url = {http://www.lri.fr/~marche/hubert05sefm.ps},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {SEFM}
}
@inproceedings{hubert07hav,
  author = {Thierry Hubert and Claude March\'e},
  title = {Separation Analysis for Deductive Verification},
  booktitle = {Heap Analysis and Verification (HAV'07)},
  year = 2007,
  address = {Braga, Portugal},
  month = mar,
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  pages = {81--93},
  url = {http://www.lri.fr/~marche/hubert07hav.pdf},
  x-pdf = {http://www.lri.fr/~marche/hubert07hav.pdf},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {HAV}
}
@inproceedings{labbe07,
  author = {S\'ebastien Labb\'e and Jean-Pierre Gallois and
                  Marc Pouzet},
  title = {Slicing Communicating Automata Specifications
                  For Efficient Model Reduction},
  booktitle = {18th Australian Conference on Software Engineering (ASWEC)},
  year = 2007,
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ASWEC}
}
@inproceedings{MandelMaranget08esop,
  author = {Louis Mandel and Luc Maranget},
  title = {Programming in {JoCaml} (Tool Demonstration)},
  crossref = {esop08},
  year = 2008,
  pages = {108--111},
  x-pdf = {http://www.lri.fr/~mandel/papers/MandelMaranget-ESOP-2008.pdf},
  url = {http://www.lri.fr/~mandel/papers/MandelMaranget-ESOP-2008.pdf},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ESOP},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@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 = {June},
  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{marche07plpv,
  author = {Claude March\'e},
  title = {Jessie: an intermediate Language for {Java} and {C} Verification},
  booktitle = {Programming Languages meets Program Verification (PLPV)},
  year = {2007},
  topics = { team},
  isbn = {978-1-59593-677-6},
  pages = {1--2},
  doi = {http://doi.acm.org/10.1145/1292597.1292598},
  url = {http://doi.acm.org/10.1145/1292597.1292598},
  publisher = {ACM},
  type_digiteo = {conf_isbn},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-support = {actes},
  x-cle-support = {PLPV},
  address = {Freiburg, Germany}
}
@inproceedings{filliatre08smt,
  author = {Jean-Christophe Filli\^atre},
  title = {{Using SMT solvers for deductive verification of C and Java programs}},
  booktitle = {{SMT 2008: 6th International Workshop on Satisfiability Modulo}},
  editor = {Clark Barrett and Leonardo de Moura},
  year = 2008,
  topics = { team},
  type_digiteo = {conf_isbn},
  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_aux},
  x-cle-support = {SMT},
  address = {Princeton, USA}
}
@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{marche07rta,
  author = {March\'e, Claude and Zantema, Hans},
  title = {The Termination Competition},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  crossref = {rta07},
  pages = {303--313},
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {RTA},
  x-pdf = {http://www.lri.fr/~marche/marche07rta.pdf},
  url = {http://www.lri.fr/~marche/marche07rta.pdf},
  x-slides = {http://www.lri.fr/~marche/marche07rta-slides.pdf}
}
@inproceedings{marche07wst,
  author = {Claude March{\'e} and Hans Zantema and Johannes Waldmann},
  title = {The Termination Competition 2007},
  crossref = {wst07},
  topics = {team},
  type_digiteo = {conf_autre},
  type_publi = {icolcomlec},
  url = {http://www.lri.fr/~marche/termination-competition/},
  note = {\url{http://www.lri.fr/~marche/termination-competition/}},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {WST}
}
@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{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{Pouzet08c,
  author = {Albert Cohen and Louis Mandel and Florence Plateau and
                  Marc Pouzet},
  title = {{Abstraction of Clocks in Synchronous Data-flow Systems}},
  booktitle = {The Sixth ASIAN Symposium on Programming Languages and Systems
              (APLAS)},
  abstract = { Synchronous data-flow languages such as Lustre manage infinite
  sequences or streams as basic values. Each stream is
  associated to a clock which defines the instants where the
  current value of the stream is present. This clock is a type
  information and a dedicated type system --- the so-called
  clock-calculus --- statically rejects programs which cannot be
  executed synchronously. In existing synchronous languages, it
  amounts at asking whether two streams have the same clocks and thus
  relies on clock equality only. Recent works have shown the interest
  of introducing some relaxed notion of synchrony, where two streams can
  be composed as soon as they can be synchronized through the
  introduction of a finite buffer (as done in the SDF model of Edward
  Lee).  This technically consists in replacing typing by
  subtyping. The present paper introduces a simple way to achieve
  this relaxed model through the use of clock
    envelopes. These clock envelopes are sets of concrete clocks which
  are not necessarily periodic. This allows to model various features
  in real-time embedded software such as bounded jitter as found in
  video-systems,  execution time of real-time processes and
  scheduling resources or the communication through buffers. We
  present the algebra of clock envelopes and its main theoretical
  properties.},
  x-pdf = {http://www.lri.fr/~plateau/papers/aplas08.pdf},
  url = {http://www.lri.fr/~plateau/papers/aplas08.pdf},
  year = 2008,
  month = dec,
  date = {9--11},
  address = { Bangalore, India},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {APLAS},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  topics = {team}
}
@inproceedings{Pouzet08b,
  author = {Gwenael Delaval and Alain Girault and Marc Pouzet},
  title = {{A Type System for the Automatic Distribution
                   of Higher-order Synchronous Dataflow Programs}},
  booktitle = {ACM International Conference on
                  Languages, Compilers, and Tools for Embedded Systems
                  (LCTES)},
  year = 2008,
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {LCTES},
  address = {Tucson, Arizona},
  month = {June},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  topics = {team}
}
@inproceedings{Pouzet08a,
  author = {Dariusz Biernacki and Jean-Louis Cola\c{c}o and Gr\'egoire Hamon
                  and Marc Pouzet},
  title = {{Clock-directed Modular Code Generation of Synchronous Data-flow
                   Languages}},
  booktitle = {ACM International Conference on
                  Languages, Compilers, and Tools for Embedded Systems
                  (LCTES)},
  year = 2008,
  address = {Tucson, Arizona},
  month = {June},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {LCTES},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  topics = {team}
}
@inproceedings{mandel05ppdp,
  author = {Louis Mandel and Marc Pouzet},
  title = {{ReactiveML, a Reactive Extension to ML}},
  booktitle = {ACM International Conference
                  on Principles and Practice of Declarative Programming
                  (PPDP)},
  year = 2005,
  pages = {82--93},
  x-pdf = {http://www.lri.fr/~mandel/papers/MandelPouzet-PPDP-2005.pdf},
  url = {http://www.lri.fr/~mandel/papers/MandelPouzet-PPDP-2005.pdf},
  topics = {team},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {PPDP},
  address = {Lisboa},
  month = jul
}
@inproceedings{MandelPlateau2008SLAP,
  author = {Louis Mandel and Florence Plateau},
  title = {Interactive Programming of Reactive Systems},
  booktitle = {Proceedings of Model-driven High-level Programming of Embedded Systems ({SLA++P'08})},
  year = 2008,
  month = apr,
  address = {Budapest, Hungary},
  pages = {44--59},
  x-pdf = {http://www.lri.fr/~mandel/papers/MandelPlateau-SLAP-2008.pdf},
  url = {http://www.lri.fr/~mandel/papers/MandelPlateau-SLAP-2008.pdf},
  topics = {team},
  type_publi = {icolcomlec},
  series = {Electronic Notes in Computer Science},
  publisher = {Elsevier Science Publishers},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {ENTCS},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{MorelMandel2007FESCA,
  author = {Lionel Morel and Louis Mandel},
  title = {Executable Contracts for Incremental Prototypes of Embedded Systems},
  booktitle = {Formal Foundations of Embedded Software
                  and Component-Based Software Architectures ({FESCA'07})},
  month = mar,
  year = 2007,
  x-pdf = {http://www.lri.fr/~mandel/papers/MorelMandel-FESCA-2007.pdf},
  url = {http://www.lri.fr/~mandel/papers/MorelMandel-FESCA-2007.pdf},
  pages = {123--136},
  topics = {team},
  type_digiteo = {conf_autre},
  type_publi = {icolcomlec},
  serie = {Electronic Notes in Computer Science},
  publisher = {Elsevier Science Publishers},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {ENTCS}
}
@inproceedings{HalbwachsMandel2006ACSD,
  author = {Nicolas Halbwachs and Louis Mandel},
  title = {Simulation and verification of asynchronous systems by means of a synchronous model},
  booktitle = {Sixth International Conference on Application of Concurrency to System Design ({ACSD'06})},
  year = {2006},
  address = {Turku, Finland},
  month = jun,
  pages = {3--14},
  x-pdf = {http://www.lri.fr/~mandel/papers/HalbwachsMandel-ACSD-2006.pdf},
  url = {http://www.lri.fr/~mandel/papers/HalbwachsMandel-ACSD-2006.pdf},
  topics = {team},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ACSD}
}
@inproceedings{SamperMaraninchiMounierMandel2006InterSense,
  author = {Ludovic Samper and Florence Maraninchi and Laurent Mounier
                  and Louis Mandel},
  title = {{GLONEMO}: Global and Accurate Formal Models for the Analysis of Ad hoc Sensor Networks},
  booktitle = {Proceedings of the First International Conference on Integrated Internet Ad hoc and Sensor Networks ({InterSense'06})},
  year = {2006},
  address = {Nice, France},
  month = may,
  publisher = {ACM},
  url = {http://www.lri.fr/~mandel/papers/SamperMaraninchiMounierMandel-InterSense-2006.pdf},
  x-pdf = {http://www.lri.fr/~mandel/papers/SamperMaraninchiMounierMandel-InterSense-2006.pdf},
  topics = {team},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {Bodynets}
}
@inproceedings{MandelBenbadis2005SLAP,
  author = {Louis Mandel and Farid Benbadis},
  title = {Simulation of Mobile Ad hoc Network Protocols in {ReactiveML}},
  booktitle = {Proceedings of Synchronous Languages, Applications, and Programming ({SLAP'05})},
  publisher = {Elsevier Science Publishers},
  year = 2005,
  month = apr,
  address = {Edinburgh, Scotland},
  x-pdf = {http://www.lri.fr/~mandel/papers/MandelBenbadis-SLAP-2005.pdf},
  url = {http://www.lri.fr/~mandel/papers/MandelBenbadis-SLAP-2005.pdf},
  topics = {team},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ENTCS}
}
@inproceedings{MandelPouzet2005JFLA,
  author = {Louis Mandel and Marc Pouzet},
  title = {{ReactiveML}, un langage pour la programmation r{\'e}active en {ML}},
  crossref = {jfla05},
  pages = {1-16},
  url = {http://www.lri.fr/~mandel/papers/MandelPouzet-JFLA-2005.ps},
  topics = {team},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@inproceedings{marche05tphols,
  topics = {team},
  author = {Claude March\'e and Christine Paulin-Mohring},
  title = {Reasoning about {Java} Programs with Aliasing and Frame
  Conditions},
  crossref = {tphols2005},
  pages = {179--194},
  topics = {team,lri},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {TPHOLs},
  url = {http://www.lri.fr/~marche/marche05tphols.ps}
}
@inproceedings{marche06sefm,
  author = {Claude March\'e and Nicolas Rousset},
  topics = {team},
  title = {Verification of {Java Card} Applets Behavior with
  respect to Transactions and Card Tears},
  crossref = {sefm06},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {SEFM},
  url = {http://www.lri.fr/~marche/marche06sefm.ps}
}
@inproceedings{marche06wst,
  author = {Claude March{\'e} and Hans Zantema},
  title = {The Termination Competition 2006},
  crossref = {wst06},
  year = 2006,
  topics = {team},
  type_publi = {icolcomlec},
  url = {http://www.lri.fr/~marche/termination-competition/},
  note = {\url{http://www.lri.fr/~marche/termination-competition/}},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {WST}
}
@inproceedings{moy07ccpp,
  author = {Yannick Moy},
  title = {Union and Cast in Deductive Verification},
  booktitle = {Proceedings of the {C/C++} Verification Workshop},
  year = 2007,
  volume = {Technical Report ICIS-R07015},
  month = jul,
  pages = {1--16},
  publisher = {Radboud University Nijmegen},
  x-pdf = {http://www.lri.fr/~moy/Publis/moy07ccpp.pdf},
  url = {http://www.lri.fr/~moy/Publis/moy07ccpp.pdf},
  type_digiteo = {conf_autre},
  type_publi = {icolcomlec},
  topics = {team, lri},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes_aux}
}
@inproceedings{moy07hav,
  author = {Yannick Moy and Claude March\'e},
  title = {Inferring Local (Non-)Aliasing and Strings for Memory Safety},
  booktitle = {Heap Analysis and Verification (HAV'07)},
  year = 2007,
  address = {Braga, Portugal},
  month = mar,
  pages = {35--51},
  topics = {team lri},
  type_digiteo = {conf_autre},
  type_publi = {icolcomlec},
  x-pdf = {http://www.lri.fr/~moy/Publis/moy07hav.pdf},
  url = {http://www.lri.fr/~moy/Publis/moy07hav.pdf},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {HAV}
}
@inproceedings{moy08vmcai,
  author = {Yannick Moy},
  title = {Sufficient Preconditions for Modular Assertion Checking},
  crossref = {vmcai08},
  pages = {188--202},
  x-pdf = {http://www.lri.fr/~moy/publis/moy08vmcai.pdf},
  url = {http://www.lri.fr/~moy/publis/moy08vmcai.pdf},
  topics = {team, lri},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {VMCAI},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{oury05tphols,
  author = {Nicolas Oury},
  title = {Extensionality in the {Calculus of Constructions}},
  topics = {team,lri},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  pages = {278--293},
  x-cle-support = {TPHOLs},
  crossref = {tphols2005}
}
@inproceedings{signoles05jfla,
  author = {Julien Signoles},
  title = {Une approche fonctionnelle du mod\`ele vue-contr\^oleur},
  topics = {team, lri},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  crossref = {jfla05},
  pages = {63--78}
}
@inproceedings{sozeau06types,
  author = {Matthieu Sozeau},
  title = {Subset coercions in {C}oq},
  year = 2007,
  crossref = {types06},
  pages = {237--252},
  url = {http://www.lri.fr/~sozeau/research/publications/Subset_Coercions_in_Coq.pdf},
  x-slides = {http://www.lri.fr/~sozeau/research/publications/Subset_Coercions_in_Coq-types06-210406.pdf},
  abstract = {We propose a new language for writing programs with dependent
  types on top of the {C}oq proof assistant. This language permits
  to establish a phase distinction between writing and proving
  algorithms in the {C}oq environment.  Concretely, this means allowing
  to write algorithms as easily as in a practical functional programming
  language whilst giving them as rich a specification as desired and
  proving that the code meets the specification using the whole {C}oq
  proof apparatus. This is achieved by extending conversion to an
  equivalence which relates types and subsets based on them, a technique
  originating from the ``Predicate subtyping'' feature of PVS
  and following mathematical convention. The typing judgements can be
  translated to the Calculus of Inductive Constructions by means of an interpretation
  which inserts coercions at the appropriate places. These coercions can
  contain existential variables representing the propositional parts of
  the final term, corresponding to proof obligations (or PVS
  type-checking conditions). A prototype implementation of this process
  is integrated with the {C}oq environment.},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {TYPES}
}
@inproceedings{sozeau07icfp,
  author = {Matthieu Sozeau},
  title = {{P}rogram-ing Finger Trees in {C}oq},
  pages = {13--24},
  doi = {http://doi.acm.org/10.1145/1291151.1291156},
  url = {http://www.lri.fr/~sozeau/research/publications/Program-ing_Finger_Trees_in_Coq.pdf},
  x-slides = {http://www.lri.fr/~sozeau/research/publications/Program-ing_Finger_Trees_in_Coq-icfp07-011007.pdf},
  copyright = {ACM, 2007. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in
   ICFP'07, http://doi.acm.org/10.1145/1291151.1291156},
  abstract = {Finger Trees (Hinze & Paterson, JFP 2006) are a general purpose persistent
data structure with good performance. Their genericity permits developing
a wealth of structures like ordered sequences or interval trees
on top of a single implementation. However, the type systems
used by current functional languages do not guarantee the coherent
parameterization and specialization of Finger Trees, let alone the
correctness of their implementation.
We present a certified implementation of Finger Trees solving
these problems using the {P}rogram extension of {C}oq.
We not only implement the structure but also prove its
invariants along the way, which permit building certified
structures on top of Finger Trees in an elegant way.},
  crossref = {icfp07},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ICFP}
}
@inproceedings{sozeau08tphols,
  author = {Matthieu Sozeau and Nicolas Oury},
  crossref = {tphols2008},
  url = {http://www.lri.fr/~sozeau/research/publications/First-Class_Type_Classes.pdf},
  x-slides = {http://www.lri.fr/~sozeau/research/publications/First-Class_Type_Classes-TPHOLs-200808.pdf},
  title = {{F}irst-{C}lass {T}ype {C}lasses},
  abstract = {
Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for
specifying with abstract structures by quantification on contexts. However,
both systems are limited by second-class implementations of these constructs,
and these limitations are only overcomed by ad-hoc extensions to
the respective systems. We propose an embedding of type classes into a
dependent type theory that is first-class and supports some of the most
popular extensions right away. The implementation is correspondingly
cheap, general and very well integrated inside the system, as we have
experimented in Coq. We show how it can be used to help structured
programming and proving by way of examples.},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {TPHOLs},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{bol08rnc,
  title = {Formal proof for delayed finite field arithmetic using floating point operators},
  author = {Sylvie Boldo and Marc Daumas and Pascal Giorgi},
  booktitle = {Proceedings of the 8th Conference on Real Numbers and
                   Computers},
  year = {2008},
  address = {Santiago de Compostela, Spain},
  month = jul,
  pages = {113--122},
  editor = {Daumas, Marc and Bruguera, Javier},
  x-pdf = {http://hal.archives-ouvertes.fr/docs/00/27/89/89/PDF/rnc.pdf},
  hal = {http://hal.inria.fr/inria-00278989/en/},
  topics = {team,lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {RNC},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{bardou08ftfjp,
  author = {Romain Bardou},
  title = {Ownership, Pointer Arithmetic and Memory Separation},
  crossref = {ftfjp08},
  topics = {team},
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {FTJP},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  url = {http://romain.bardou.fr/papers/jcown.pdf}
}
@inproceedings{bol05arith,
  author = {Sylvie Boldo and Jean-Michel Muller},
  title = {Some Functions Computable with a Fused-mac},
  year = 2005,
  address = {Cape Cod, USA},
  booktitle = {Proceedings of the 17th Symposium on Computer Arithmetic},
  url = {http://perso.ens-lyon.fr/jean-michel.muller/FmacArith.pdf},
  editor = {Montuschi, Paolo and Schwarz, Eric},
  pages = {52-58},
  topics = {team,lri},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ARITH},
  type_publi = {icolcomlec}
}
@inproceedings{cohen05emsoft,
  crossref = {pouzet05emsoft}
}
@inproceedings{pouzet05emsoft,
  author = {Albert Cohen and Marc Duranton and Christine Eisenbeis
                  and Claire Pagetti and Florence Plateau and Marc Pouzet},
  title = {Synchronizing Periodic Clocks},
  booktitle = {ACM International Conference on
                  Embedded Software (EMSOFT'05)},
  address = {Jersey city, New Jersey, USA},
  month = sep,
  topics = {team},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {EMSOFT},
  year = 2005
}
@inproceedings{colaco05emsoft,
  author = {Jean-Louis Cola\c{c}o and Bruno Pagano and Marc Pouzet},
  title = {{A Conservative Extension of Synchronous Data-flow with
                   State Machines}},
  booktitle = {ACM International Conference on
                  Embedded Software (EMSOFT'05)},
  address = {Jersey city, New Jersey, USA},
  month = sep,
  topics = {team},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {EMSOFT},
  year = 2005
}
@inproceedings{cohen06popl,
  crossref = {pouzet06popl}
}
@inproceedings{pouzet06popl,
  author = {Albert Cohen and Marc Duranton and Christine Eisenbeis
                  and Claire Pagetti and Florence Plateau and Marc Pouzet},
  title = {{N-Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems}},
  booktitle = {ACM International Conference on
                  Principles of Programming Languages (POPL'06)},
  address = {Charleston, South Carolina, USA},
  month = {January},
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {POPL},
  year = 2006
}
@inproceedings{colaco06emsoft,
  author = {Jean-Louis Cola\c{c}o and Gr\'egoire Hamon and Marc Pouzet},
  title = {{Mixing Signals and Modes in Synchronous
                   Data-flow Systems}},
  booktitle = {ACM International Conference on
                  Embedded Software (EMSOFT'06)},
  address = {Seoul, South Korea},
  month = {October},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {EMSOFT},
  topics = {team},
  year = 2006
}
@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{lescuyer08tpholset,
  author = {St\'ephane Lescuyer and Sylvain Conchon},
  title = {A Reflexive Formalization of a {SAT} Solver in {Coq}},
  booktitle = {Emerging Trends of the 21st International Conference on Theorem Proving in Higher Order Logics},
  year = 2008,
  topics = {team},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {?},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{boldo06scan,
  author = {Sylvie Boldo and Marc Daumas and William Kahan and
                  Guillaume Melquiond},
  title = {Proof and certification for an accurate discriminant},
  booktitle = {12th IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics},
  year = {2006},
  address = {Duisburg,Germany},
  topics = {team},
  type_publi = {colloque},
  url = {http://scan2006.uni-due.de/show_abstracts.php?title=+Proof+and+certification+for+an+accurate+discriminant},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {SCAN},
  month = {sep}
}
@inproceedings{mlpost09jfla,
  author = {Romain Bardou and Jean-Christophe Filli\^atre and Johannes Kanig and St\'ephane Lescuyer},
  title = {{Faire bonne figure avec Mlpost}},
  url = {http://www.lri.fr/~filliatr/ftp/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{regis-gianas-pottier-08,
  author = {Yann R\'egis-Gianas and Fran\c{c}ois Pottier},
  title = {A {Hoare} Logic for Call-by-Value Functional
                 Programs},
  year = {2008},
  url = {http://cristal.inria.fr/~fpottier/publis/regis-gianas-pottier-hoarefp.pdf},
  doi = {http://dx.doi.org/10.1007/978-3-540-70594-9_17},
  pages = {305--335},
  topics = {team},
  abstract = {We present a Hoare logic for a call-by-value
                 programming language equipped with recursive,
                 higher-order functions, algebraic data types, and a
                 polymorphic type system in the style of Hindley and
                 Milner. It is the theoretical basis for a tool that
                 extracts proof obligations out of programs annotated
                 with logical assertions. These proof obligations,
                 expressed in a typed, higher-order logic, are
                 discharged using off-the-shelf automated or interactive
                 theorem provers. Although the technical apparatus that
                 we exploit is by now standard, its application to
                 functional programming languages appears to be new, and
                 (we claim) deserves attention. As a sample application,
                 we check the partial correctness of a balanced binary
                 search tree implementation.},
  booktitle = {Proceedings of the Ninth International Conference on
                 Mathematics of Program Construction (MPC'08)},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {MPC},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@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},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-support = {actes},
  topics = {team}
}
@inproceedings{boldo09icalp,
  author = {Sylvie Boldo},
  title = {Floats \& {R}opes: a case study for formal numerical program
  verification},
  booktitle = {36th International Colloquium on Automata, Languages and Programming },
  pages = {91--102},
  year = {2009},
  volume = {5556},
  month = jul,
  series = {Lecture Notes in Computer Science - ARCoSS},
  publisher = {Springer},
  address = {Rhodos, Greece},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-support = {actes},
  topics = {team}
}
@inproceedings{ayad10ijcar,
  author = {Ali Ayad and Claude March\'e},
  title = {Multi-Prover Verification of Floating-Point Programs},
  crossref = {ijcar10},
  pages = {127--141},
  url = {http://www.lri.fr/~marche/ayad10ijcar.pdf},
  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{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}
}
@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 = {http://www.lri.fr/~filliatr/ftp/publis/wml09.pdf},
  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{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},
  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},
  crossref = {postfoveoos10}
}
@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 = {http://dx.doi.org/10.1007/978-3-642-04222-5_18},
  crossref = {frocos09}
}
@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{MandelPlateau-MPC-2012,
  author = {Louis Mandel and Florence Plateau},
  title = {Scheduling and Buffer Sizing of n-Synchronous Systems: 
           Typing of Ultimately Periodic Clocks in {Lucy-n}},
  booktitle = {Eleventh International Conference on Mathematics of Program Construction ({MPC'12})},
  year = 2012,
  month = jun,
  address = {Madrid, Spain},
  url = {http://www.lri.fr/~mandel/papiers/MandelPlateau-MPC-2012.pdf},
  abstract = {Lucy-n is a language for programming networks of processes
    communicating through bounded buffers. A dedicated type
    system, termed a clock calculus, automatically computes static
    schedules of the processes and the sizes of the buffers between
    them.

    In this article, we present a new algorithm which solves the
    subtyping constraints generated by the clock calculus. The
    advantage of this algorithm is that it finds schedules for tightly
    coupled systems. Moreover, it does not overestimate the buffer
    sizes needed and it provides a way
    to favor either system throughput or buffer size minimization.},
  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},
  x-equipes = {demons PROVAL EXT},
  x-support = {actes},
  x-type = {article},
  x-cle-support = {DATE},
  topics = {team},
  crossref = {date10}
}
@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},
  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 = {June},
  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}
}
@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 = {Proceedings of the first Interactive Theorem Proving Conference},
  year = 2010,
  series = {LNCS},
  address = {Edinburgh, Scotland},
  month = jul,
  publisher = {Springer},
  editor = {Matt Kaufmann and Lawrence C. Paulson},
  volume = {6172},
  pages = {147--162},
  note = {(merge of TPHOLs and ACL2)},
  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},
  hal = {http://hal.inria.fr/inria-00450789/en/}
}
@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{herms12vstte,
  title = {A Certified Multi-prover Verification Condition Generator},
  author = {Paolo Herms and Claude March{\'e} and Benjamin Monate},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-equipes = {demons PROVAL ext},
  x-support = {actes},
  x-cle-support = {VSTTE},
  x-type = {article},
  url = {http://proval.lri.fr/publications/herms12vstte.pdf},
  topics = {team},
  crossref = {vstte12}
}
@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},
  editor = {Yves Bertot},
  x-equipes = {demons PROVAL},
  x-support = {actes_aux},
  x-cle-support = {COQ},
  x-type = {article},
  topics = {team}
}
@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 = {http://www.lri.fr/~filliatr/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{filliatre10-opencert,
  author = {M. Barbosa and Jean-Christophe Filli\^atre and J. Sousa Pinto and B. 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}
}
@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 = {June},
  url = {http://proval.lri.fr/publications/dross11tap.pdf},
  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 K. 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.}
}
@inproceedings{boogie11why3,
  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},
  topics = {team},
  booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages},
  year = 2011,
  address = {Wroc\l{}aw, Poland},
  month = {August},
  pages = {53--64},
  url = {http://proval.lri.fr/publications/boogie11final.pdf},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-cle-support = {BOOGIE},
  x-type = {actes_aux},
  x-support = {article},
  x-equipes = {demons PROVAL},
  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},
  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},
  url = {http://www.lri.fr/~melquion/doc/11-arith20-article.pdf},
  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},
  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}
}
@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{filliatre12vstte,
  author = {Jean-Christophe Filli\^atre},
  title = {Verifying Two Lines of {C} with {Why3}: an Exercise in Program Verification},
  booktitle = {Verified Software: Theories, Tools and Experiments (VSTTE)},
  month = {January},
  year = 2012,
  address = {Philadelphia, USA},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-equipes = {demons PROVAL ext},
  x-support = {actes},
  x-cle-support = {VSTTE},
  x-type = {article},
  topics = {team},
  url = {http://proval.lri.fr/publications/filliatre12vstte.pdf},
  abstract = {This article details the formal verification of a 2-line C program
  that computes the number of solutions to the $n$-queens problem.
  The formal proof of (an abstraction of) the C code
  is performed using the Why3 tool to generate
  the verification conditions and several provers (Alt-Ergo, CVC3,
  Coq) to discharge them. The main purpose of this article is to
  illustrate the use of Why3 in verifying an algorithmically complex
  program.}
}
@inproceedings{lelay12jfla,
  author = {Catherine Lelay and Guillaume Melquiond},
  title = {Diff\'erentiabilit\'e et int\'egrabilit\'e en {C}oq. {A}pplication \`a la formule de d'{A}lembert},
  topics = {team, lri},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  crossref = {jfla12},
  hal = {http://hal.inria.fr/hal-00642206/fr/}
}
@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{baelde12itp,
  title = {{Towards Provably Robust Watermarking}},
  author = {David Baelde and Pierre Courtieu and David Gross-Amblard and Christine Paulin-Mohring},
  abstract = {{Watermarking techniques are used to help identifying copies of publicly released information. They consist in applying a slight and secret modification to the data before its release, in a way that should be robust, ie., remain recognizable even in (reasonably) modified copies of the data. In this paper, we present new results about the robustness of watermarking schemes against arbitrary attackers, and the formalization of those results in Coq. We used the ALEA library, which formalizes probability theory and models probabilistic programs using a simple monadic translation. This work illustrates the strengths and particularities of the induced style of reasoning about probabilistic programs. Our technique for proving robustness is adapted from methods commonly used for cryptographic protocols, and we discuss its relevance to the field of watermarking.}},
  keywords = {watermarking, probabilistic algorithms, formal proofs, security, interactive theorem proving},
  year = 2012,
  topics = {team},
  x-equipes = {demons PROVAL ext},
  month = aug,
  pdf = {http://hal.inria.fr/hal-00682398/PDF/techreport.pdf},
  booktitle = {ITP 2012}
}
@inproceedings{mentre12abz,
  author = {David Mentr\'e and Claude March\'e and Jean-Christophe Filli\^atre and Masashi Asuka},
  title = {Discharging Proof Obligations from {Atelier~B} using
  Multiple Automated Provers},
  booktitle = {ABZ'2012 - 3rd International Conference on Abstract State Machines, Alloy, B and Z},
  series = {Lecture Notes in Computer Science},
  editor = {Steve Reeves and Elvinia Riccobene},
  publisher = {Springer},
  optvolume = {?},
  optpages = {?--?},
  year = 2012,
  address = {Pisa, Italy},
  month = {June},
  abstract = {We present a method to discharge proof obligations from Atelier~B
  using multiple SMT solvers. It is based on a faithful modeling of
  B's set theory into polymorphic first-order logic. We report on two
  case studies demonstrating a significant improvement in the ratio of
  obligations that are automatically discharged.},
  obsoletepdf = {http://www.lri.fr/~filliatr/publis/abz12.pdf},
  topics = {team},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-equipes = {demons PROVAL ext},
  x-cle-support = {ABZ},
  x-pays = {jp},
  hal_id = {hal-00681781},
  hal = {http://hal.inria.fr/hal-00681781/en/},
  note = {\url{http://hal.inria.fr/hal-00681781/en/}}
}
@inproceedings{bormer11foveoos,
  author = {Thorsten Bormer and Marc Brockschmidt and Dino Distefano and Gidon Ernst and Jean-Christophe Filli\^atre and Radu Grigore and Marieke Huisman and Vladimir Klebanov and Claude March\'e and Rosemary Monahan and Wojciech Mostowski and Nadia Polikarpova and Christoph Scheben and Gerhard Schellhorn and Bogdan Tofan and Julian Tschannen and Mattias Ulbrich},
  title = {The {COST IC0701} Verification Competition 2011},
  url = {http://proval.lri.fr/publications/bormer12foveoos.pdf},
  crossref = {postfoveoos11},
  topics = {team}
}
@inproceedings{filliatre12aipa,
  author = {Jean-Christophe Filli\^atre},
  title = {{Combining Interactive and Automated Theorem Proving
in Why3 (invited talk)}},
  booktitle = {{Automation in Proof Assistants 2012}},
  editor = {Keijo Heljanko and Hugo Herbelin},
  month = {April},
  year = 2012,
  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},
  address = {Tallinn, Estonia}
}
@inproceedings{conchon12cav,
  author = {Sylvain Conchon and Amit Goel and Sava Krsti{\'c}
                  and Alain Mebsout and Fatiha Za{\"i}di},
  title = {{Cubicle}: A Parallel {SMT}-based Model Checker for
                  Parameterized Systems},
  booktitle = {CAV 2012: Proceedings of the 24th International Conference on Computer Aided Verification},
  year = {2012},
  topics = {team},
  editor = {Madhusudan Parthasarathy and Sanjit A. Seshia},
  series = {Lecture Notes in Computer Science},
  month = jul,
  address = {Berkeley, California, USA},
  publisher = {Springer},
  abstract = { Cubicle is a new model checker for verifying safety
                  properties of parameterized systems. It implements a
                  parallel symbolic backward reachability procedure
                  using Satisfiabilty Modulo Theories.  Experiments
                  done on classic and challenging mutual exclusion
                  algorithms and cache coherence protocols show that
                  Cubicle is effective and competitive with
                  state-of-the-art model checkers.}
}
@inproceedings{bobot12ijcar,
  author = {Fran\c{c}ois Bobot and Sylvain Conchon and
  Evelyne Contejean and Mohamed Iguernelala and
  Assia Mahboubi and Alain Mebsout and Guillaume Melquiond},
  title = {A {Simplex}-Based Extension of {Fourier-Motzkin} for
                  Solving Linear Integer Arithmetic},
  booktitle = {IJCAR 2012: Proceedings of the 6th International Joint
                  Conference on Automated Reasoning},
  year = {2012},
  editor = {Bernhard Gramlich and Dale Miller and Ulrike Sattler},
  series = {Lecture Notes in Computer Science},
  address = {Manchester, UK},
  month = jun,
  volume = {7364},
  pages = {67--81},
  doi = {10.1007/978-3-642-31365-3_8},
  topics = {team},
  type_publi = {icolcomlec},
  publisher = {Springer},
  abstract = {This paper describes a novel decision procedure for
                  quantifier-free linear integer arithmetic. Standard
                  techniques usually relax the initial problem to the
                  rational domain and then proceed either by
                  projection (e.g. Omega-Test) or by branching/cutting
                  methods (branch-and-bound, branch-and-cut, Gomory
                  cuts). Our approach tries to bridge the gap between
                  the two techniques: it interleaves an exhaustive
                  search for a model with bounds inference. These
                  bounds are computed provided an oracle capable of
                  finding constant positive linear combinations of
                  affine forms. We also show how to design an
                  efficient oracle based on the Simplex procedure. Our
                  algorithm is proved sound, complete, and terminating
                  and is implemented in the Alt-Ergo theorem
                  prover. Experimental results are promising and show
                  that our approach is competitive with
                  state-of-the-art SMT solvers.}
}
@inproceedings{filliatre12compare,
  author = {Jean-Christophe Filli\^atre and Andrei Paskevich and Aaron Stump},
  title = {The 2nd Verified Software Competition: Experience Report},
  booktitle = {COMPARE2012: 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems},
  address = {Manchester, UK},
  month = {June},
  year = 2012,
  editor = {Vladimir Klebanov and Sarah Grebing},
  publisher = {EasyChair},
  type_publi = {icolcomlec},
  topics = {team},
  abstract = {We report on the second verified software competition.  It was
  organized by the three authors on a 48 hours period on November
  8--10, 2011. This paper describes the competition, presents the five
  problems that were proposed to the participants, and gives an
  overview of the solutions sent by the 29 teams that entered the
  competition.},
  url = {http://www.lri.fr/~filliatr/pub/compare2012.pdf}
}
@inproceedings{filliatre12inforum,
  author = {M\'ario Pereira and Jean-Christophe Filli\^atre and
    Sim{\~a}o Melo de Sousa},
  title = {{ARMY}: a Deductive Verification Platform for {ARM} Programs Using {Why3}},
  month = {September},
  year = 2012,
  type_publi = {icolcomlec},
  topics = {team},
  abstract = {Unstructured (low-level) programs tend to be challenging
    to prove correct, since the control flow is
    arbitrary complex and there are no obvious points in
    the code where to insert logical assertions. In this
    paper, we present a system to formally verify ARM
    programs, based on a flow sequentialization
    methodology and a formalized ARM semantics. This
    system, built upon the why3 verification platform,
    takes an annotated ARM program, turns it into a set
    of purely sequential flow programs, translates these
    programs' instructions into the corresponding
    formalized opcodes and finally calls the Why3 VCGen
    to generate the verification conditions that can
    then be discharged by provers. A prototype has been
    implemented and used to verify several programming
    examples.},
  booktitle = {INForum 2012}
}
@inproceedings{bobot12icfem,
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre},
  title = {Separation Predicates: a Taste of Separation Logic in
    First-Order Logic},
  booktitle = {14th International Conference on Formal Ingineering Methods
   (ICFEM)},
  volume = 7635,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  address = {Kyoto, Japan},
  month = {November},
  year = 2012,
  type_publi = {icolcomlec},
  topics = {team},
  abstract = {This paper introduces \emph{separation predicates}, a technique to
  reuse some ideas from separation logic in the framework of program
  verification using a traditional first-order logic.  The purpose is
  to benefit from existing specification languages, verification
  condition generators, and automated theorem provers.
  Separation predicates are automatically derived
  from user-defined inductive predicates.
  We illustrate
  this idea on a non-trivial case study, namely the composite pattern,
  which is specified in C/ACSL and verified in a fully automatic way
  using SMT solvers Alt-Ergo, CVC3, and Z3.},
  url = {http://proval.lri.fr/publications/bobot12icfem.pdf}
}
@inproceedings{boldo12cpp,
  author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
  title = {{Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives}},
  booktitle = {Proceedings of the The Second International Conference on Certified Programs and Proofs},
  optpages = {},
  year = {2012},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  address = {Kyoto, Japan},
  month = dec,
  optorganization = {},
  optpublisher = {},
  optnote = {},
  hal = {http://hal.inria.fr/hal-00712938},
  topics = {team}
}
@inproceedings{conchon12smt,
  author = {Sylvain Conchon and Guillaume Melquiond and Cody Roux and Mohamed Iguernelala},
  title = {Built-in Treatment of an Axiomatic Floating-Point Theory for {SMT} Solvers},
  crossref = {smt2012},
  topics = {team}
}
@inproceedings{dross12smt,
  author = {Claire Dross and Sylvain Conchon and Johannes Kanig and Andrei Paskevich},
  title = {Reasoning with Triggers},
  crossref = {smt2012},
  topics = {team}
}
@inproceedings{cousineau12fm,
  author = {Denis Cousineau and
               Damien Doligez and
               Leslie Lamport and
               Stephan Merz and
               Daniel Ricketts and
               Hern{\'a}n Vanzetto},
  title = {{TLA+} Proofs},
  pages = {147--154},
  x-equipes = {demons PROVAL ext},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {FM},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  topics = {team},
  crossref = {fm2012}
}
@inproceedings{cousineau12rta,
  author = {Denis Cousineau and Olivier Hermant},
  title = {A Semantic Proof that Reducibility Candidates entail Cut
               Elimination},
  pages = {133--148},
  ee = {http://dx.doi.org/10.4230/LIPIcs.RTA.2012.133},
  crossref = {rta12},
  x-equipes = {demons PROVAL ext},
  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{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},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  crossref = {popl13}
}
@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{afm07,
  title = {{Proceedings of the second workshop on Automated formal methods}},
  booktitle = {{Proceedings of the second workshop on Automated formal methods}},
  year = 2007,
  editor = {John Rushby and N. Shankar},
  publisher = {ACM Press},
  isbn = {978-1-59593-879-4}
}
@proceedings{cade05,
  title = {20th International Conference on Automated Deduction},
  booktitle = {20th International Conference on Automated Deduction (CADE-20)},
  address = {Tallinn, Estonia},
  month = jul,
  year = 2005,
  editor = {Robert Nieuwenhuis},
  series = {Lecture Notes in Artificial Intelligence},
  volume = 3632,
  publisher = {Springer},
  isbn = {3-540-28005-7}
}
@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{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{rta04,
  title = {15th International Conference on Rewriting Techniques and Applications},
  booktitle = {15th International Conference on Rewriting Techniques and Applications},
  editor = {Vincent van Oostrom},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 3091,
  month = jun,
  year = 2004,
  address = {Aachen, Germany},
  isbn = {3-540-22153-0}
}
@proceedings{rta11,
  booktitle = {22nd International Conference on Rewriting Techniques and Applications (RTA 11)},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  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{rta12,
  title = {23rd International Conference on Rewriting Techniques and Applications},
  booktitle = {23nd International Conference on Rewriting Techniques and Applications},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  year = {2012},
  volume = {15},
  editor = {Ashish Tiwari},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address = {Nagoya, Japan},
  isbn = {978-3-939897-38-5}
}
@proceedings{ijcar06,
  title = {International Joint Conference on Automated Reasoning},
  booktitle = {Third International Joint Conference on Automated Reasoning},
  editor = {Ulrich Furbach and Natarajan Shankar},
  year = 2006,
  series = {Lecture Notes in Computer Science},
  volume = 4130,
  address = {Seattle, USA},
  month = aug,
  publisher = {Springer}
}
@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{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{tphols2005,
  title = {Theorem Proving in Higher Order Logics:
                           18th International Conference, TPHOLs 2005},
  booktitle = {18th International Conference on Theorem Proving in Higher Order Logics},
  editor = {J. Hurd and T. Melham},
  series = {Lecture Notes in Computer Science},
  year = 2005,
  volume = 3603,
  addresse = {Oxford, UK},
  month = aug,
  publisher = {Springer}
}
@proceedings{tphols2008,
  title = {Theorem Proving in Higher Order Logics:
                           21th International Conference, TPHOLs 2008},
  booktitle = {21th International Conference on Theorem Proving in Higher Order Logics},
  editor = {Otmame A{\"i}t-Mohamed and C\'esar Mu{\~n}oz and Sofi\`ene Tahar},
  series = {Lecture Notes in Computer Science},
  volume = 5170,
  year = 2008,
  addresse = {Montr\'eal, Canada},
  month = aug,
  publisher = {Springer}
}
@proceedings{types03,
  editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
  title = {3rd International Workshop on Types for Proofs and Programs},
  booktitle = {3rd International Workshop on Types for Proofs and Programs},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 3085,
  year = 2004,
  isbn = {3-540-22164-6},
  month = apr,
  address = {Torino, Italy}
}
@proceedings{types06,
  editor = {Thorsten Altenkirch and Conor Mc Bride},
  title = {Types for Proofs and Programs, International Workshop, TYPES
               2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES
               2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4502},
  year = {2007},
  isbn = {978-3-540-74463-4}
}
@proceedings{wst06,
  booktitle = {{Extended Abstracts of the 8th International Workshop on Termination, WST'06}},
  title = {{Extended Abstracts of the 8th International Workshop on Termination, WST'06}},
  year = {2006},
  editor = {Alfons Geser and Harald Sondergaard},
  month = aug
}
@proceedings{wst07,
  booktitle = {{Extended Abstracts of the 9th International Workshop on Termination, WST'07}},
  title = {{Extended Abstracts of the 9th International Workshop on Termination, WST'07}},
  year = {2007},
  editor = {Dieter Hofbauer and Alexander Serebrenik},
  month = jun
}
@proceedings{amast04,
  title = {Algebraic Methodology and Software Technology},
  booktitle = {Algebraic Methodology and Software Technology},
  year = 2004,
  series = {Lecture Notes in Computer Science},
  volume = 3116,
  address = {Stirling, UK},
  month = jul,
  publisher = {Springer}
}
@proceedings{pepm04,
  title = {Partial Evaluation and Program Manipulation},
  year = 2004,
  booktitle = {ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation},
  address = {Verona, Italy},
  month = aug,
  publisher = {ACM Press}
}
@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{icfem04,
  title = {Formal Engineering Methods},
  year = 2004,
  booktitle = {6th International Conference on Formal Engineering Methods},
  series = {Lecture Notes in Computer Science},
  volume = 3308,
  editor = {Jim Davies and Wolfram Schulte and Mike Barnett},
  address = {Seattle, WA, USA},
  month = nov,
  publisher = {Springer}
}
@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{cav07,
  editor = {Werner Damm and Holger Hermanns},
  title = {Computer Aided Verification},
  booktitle = {19th International Conference on Computer Aided Verification},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 4590,
  address = {Berlin, Germany},
  month = jul,
  year = {2007}
}
@proceedings{jfla05,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2005,
  booktitle = {Seizi\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = mar,
  publisher = {INRIA}
}
@proceedings{jfla06,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2006,
  booktitle = {Dix-septi\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  publisher = {INRIA}
}
@proceedings{jfla07,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2007,
  booktitle = {Dix-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  publisher = {INRIA}
}
@proceedings{jfla08,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2008,
  booktitle = {Dix-neuvi\`emes  Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  publisher = {INRIA}
}
@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{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{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{jfla12,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2012,
  booktitle = {Vingt-troisi\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = feb,
  address = {Carnac, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes}
}
@proceedings{sefm05,
  title = {Software Engineering and Formal Methods},
  year = 2005,
  booktitle = {3rd IEEE International Conference on Software Engineering
and Formal Methods (SEFM'05)},
  address = {Koblenz, Germany},
  editor = {Bernhard K. Aichernig and Bernhard Beckert},
  publisher = {{IEEE} Comp. Soc. Press},
  month = sep
}
@proceedings{sefm06,
  title = {Software Engineering and Formal Methods},
  year = 2006,
  editor = {Dang Van Hung and Paritosh Pandya},
  booktitle = {4th IEEE International Conference on Software Engineering
and Formal Methods (SEFM'06)},
  address = {Pune, India},
  publisher = {{IEEE} Comp. Soc. Press},
  month = sep
}
@proceedings{rta07,
  editor = {Franz Baader},
  title = {Term Rewriting and Applications},
  booktitle = {18th International Conference on Rewriting Techniques and Applications (RTA'07)},
  address = {Paris, France},
  month = jun,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 4533,
  year = 2007
}
@proceedings{fm05,
  editor = {John Fitzgerald and Ian J. Hayes and Andrzej Tarlecki},
  title = {Formal Methods},
  booktitle = {International Symposium of Formal Methods Europe (FM'05)},
  address = {Newcastle,UK},
  month = jul,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3582},
  year = 2005
}
@proceedings{mpc2006,
  editor = {Tarmo Uustalu},
  title = {Mathematics of Program Construction, 8th International Conference,
               MPC 2006},
  booktitle = {Mathematics of Program Construction, MPC 2006},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  month = jul,
  address = {Kuressaare, Estonia},
  volume = {4014},
  year = {2006}
}
@proceedings{icfp07,
  editor = {Ralf Hinze and Norman Ramsey},
  title = {Proceedings of the 12th ACM SIGPLAN International Conference
               on Functional Programming, ICFP 2007},
  booktitle = {12th ACM SIGPLAN International Conference
               on Functional Programming, ICFP 2007},
  address = {Freiburg, Germany},
  publisher = {ACM Press},
  year = {2007},
  isbn = {978-1-59593-815-2}
}
@proceedings{icfp08,
  editor = {James Hook and Peter Thiemann},
  title = {Proceeding of the 13th ACM SIGPLAN international conference
               on Functional programming, ICFP 2008},
  booktitle = {13th ACM SIGPLAN international conference
               on Functional programming, ICFP 2008},
  address = {Victoria, BC, Canada},
  publisher = {ACM},
  year = {2008},
  month = sep,
  isbn = {978-1-59593-919-7}
}
@proceedings{frocos07,
  editor = {Boris Konev and Frank Wolter},
  title = {6th International Symposium on Frontiers of Combining Systems (FroCos 07)},
  booktitle = {6th International Symposium on Frontiers of Combining Systems (FroCos 07)},
  month = sep,
  year = 2007,
  address = {Liverpool,UK},
  publisher = {Springer},
  series = {Lecture Notes in Artificial Intelligence},
  volume = 4720,
  isbn = {978-3-540-74620-1}
}
@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}
}
@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{vmcai08,
  editor = {Francesco Logozzo and Doron Peled and Lenore Zuck},
  title = {Verification, Model Checking, and Abstract Interpretation},
  booktitle = {9th International Conference on Verification, Model Checking, and Abstract Interpretation},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 4905,
  address = {San Francisco, California, USA},
  month = jan,
  year = {2008}
}
@proceedings{esop08,
  title = {17th European Symposium on Programming (ESOP'08)},
  booktitle = {17th European Symposium on Programming (ESOP'08)},
  year = 2008,
  address = {Budapest, Hungary},
  month = apr
}
@proceedings{ftfjp08,
  title = {Formal Techniques for Java-like Programs},
  year = 2008,
  booktitle = {Formal Techniques for Java-like Programs (FTfJP'08)},
  address = {Paphos, Cyprus},
  month = jul
}
@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,
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-editorial-board = {yes},
  x-pays = {DE}
}
@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{postfoveoos11,
  editor = {Bernhard Beckert and Ferruccio Damiani and Dilian Gurov},
  title = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011},
  booktitle = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  todo-volume = {},
  year = 2012,
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-support = {actes},
  x-cle-support = {FOVEOOS}
}
@proceedings{fast05,
  booktitle = {Proceedings of FAST'05},
  year = 2005,
  editor = {R.~Gorrieri and F.~Martinelli and P.~Ryan and S.~Schneider},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = {3866}
}
@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{vstte12,
  booktitle = {VSTTE},
  year = 2012,
  editor = {Rajeev Joshi and Peter M{\"u}ller and Andreas Podelski},
  series = {Lecture Notes in Computer Science},
  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}
}
@proceedings{smt2012,
  booktitle = {SMT workshop},
  editor = {Pascal Fontaine and Amit Goel},
  publisher = {\url{http://smt2012.loria.fr/}},
  year = 2012,
  address = {Manchester, UK}
}
@proceedings{fm2012,
  editor = {Dimitra Giannakopoulou and Dominique M{\'e}ry},
  title = {FM 2012: Formal Methods - 18th International Symposium},
  booktitle = {18th International Symposium on Formal Methods},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 7436,
  year = 2012,
  isbn = {978-3-642-32758-2},
  ee = {http://dx.doi.org/10.1007/978-3-642-32759-9}
}