complete-conference.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -oc complete-conference.cite -ob complete-conference.bib -c 'topics : "team" and $type="inproceedings" and year>=2004' /home/marche/biblio/abbrevs.bib /home/marche/biblio/demons.bib /home/marche/biblio/demons2.bib /home/marche/biblio/demons3.bib /home/marche/biblio/team.bib /home/marche/biblio/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{boldo15icfem,
  title = {{Formal Verification of Programs Computing the Floating-Point Average}},
  author = {Sylvie Boldo},
  hal = {https://hal.inria.fr/hal-01174892},
  booktitle = {{17th International Conference on Formal Engineering Methods}},
  address = {Paris, France},
  publisher = {{Springer}},
  year = {2015},
  month = nov,
  pdf = {https://hal.inria.fr/hal-01174892/file/article.pdf},
  topics = {team,lri},
  type_publi = {irevcomlec},
  editor = {Michael Butler and Sylvain Conchon and Fatiha Za\"idi},
  volume = {9407},
  series = {Lecture Notes in Computer Science},
  pages = {17--32}
}
@inproceedings{bol15nsv,
  author = {Sylvie Boldo},
  title = {Stupid is as Stupid Does: Taking the Square Root of the Square
    of a Floating-Point Number},
  booktitle = {Proceedings of the Seventh and Eighth International Workshop on Numerical Software Verification},
  pages = {50--55},
  year = {2015},
  editor = {Sergiy Bogomolov and Matthieu Martel},
  series = {Electronic Notes in Theoretical Computer Science},
  address = {Seattle, WA, USA},
  month = apr,
  hal = {http://hal.inria.fr/hal-01148409},
  topics = {team,lri},
  type_publi = {irevcomlec},
  doi = {http://dx.doi.org/10.1016/j.entcs.2015.10.004},
  volume = {317}
}
@inproceedings{boldo14scan,
  hal = {https://hal.inria.fr/hal-01088692},
  title = {Formal verification of tricky numerical computations},
  author = {Sylvie Boldo},
  year = 2014,
  booktitle = {16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics},
  address = {Würzburg, Germany},
  month = sep,
  note = {Invited talk},
  url = {http://www.scan2014.uni-wuerzburg.de/book_of_abstracts/},
  topics = {team,lri},
  type_publi = {colloque}
}
@inproceedings{Lelay13,
  hal = {http://hal.inria.fr/hal-00880212},
  author = {Catherine Lelay},
  title = {{A New Formalization of Power Series in Coq}},
  booktitle = {5th Coq Workshop},
  pages = {1--2},
  year = {2013},
  address = {Rennes, France},
  month = jul,
  note = {\url{http://coq.inria.fr/coq-workshop/2013#Lelay}},
  topics = {team}
}
@inproceedings{benzaken14esop,
  hal = {http://hal.inria.fr/hal-00924156},
  author = {V\'eronique Benzaken and \'Evelyne Contejean and Stefania Dumbrava},
  title = {A {Coq} Formalization of the Relational Data Model},
  crossref = {esop2014},
  year = 2014,
  month = apr,
  editor = {Z. Shao},
  booktitle = {European Symposium on Programming, LNCS 8410},
  pages = {189-208},
  type_publi = {icolcomlec},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-support = {actes}
}
@inproceedings{benzaken08ppdp,
  author = {V. Benzaken and G.Castagna and D. Colazzo and C. Miachon},
  title = {Pattern by Example: Type-driven Visual Programming of {XML} Queries".},
  booktitle = {10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming},
  year = 2008,
  address = {Valencia, Spain},
  month = {July},
  publisher = {ACM Press},
  topics = {team, lri},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {PPDP},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@inproceedings{conchon11tacas,
  author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
  title = {{Canonized Rewriting and Ground AC Completion Modulo Shostak Theories}},
  crossref = {tacas2011},
  year = 2011,
  month = apr,
  type_publi = {icolcomlec},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-support = {actes},
  x-cle-support = {TACAS},
  url = {http://proval.lri.fr/publications/conchon11tacas.pdf},
  hal = {http://hal.inria.fr/hal-00777663},
  pages = {45-59},
  doi = {10.1007/978-3-642-19835-9_6},
  abstract = {http://www.lri.fr/~contejea/publis/2011tacas/abstract.html}
}
@inproceedings{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},
  hal = {http://hal.inria.fr/inria-00532552},
  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},
  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)}},
  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 = jun,
  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 = jun,
  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 = {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 = {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 = {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 Press},
  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 Press},
  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 = {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 = {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 = {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 = {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},
  hal = {http://hal.inria.fr/hal-00777669},
  urn = {urn:nbn:de:0030-drops-31192},
  doi = {10.4230/LIPIcs.RTA.2011.21},
  pages = {21--30},
  abstract = {http://www.lri.fr/~contejea/publis/2011rta/abstract.html},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {RTA},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  topics = {team}
}
@inproceedings{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 = jun,
  address = {Dublin},
  booktitle = {ACM International Conference on
                  Languages, Compilers, and Tools for Embedded Systems
                  (LCTES)},
  x-type = {article},
  topics = {team},
  x-support = {actes},
  x-equipes = {demons PROVAL ext}
}
@inproceedings{lucy:emsoft09,
  author = {Marc Pouzet and Pascal Raymond},
  title = {Modular Static Scheduling of Synchronous Data-flow
                  Networks: An efficient symbolic representation},
  booktitle = {ACM International Conference on
                  Embedded Software (EMSOFT'09)},
  address = {Grenoble, France},
  month = {October},
  year = 2009,
  topics = {team},
  x-type = {article},
  x-support = {actes},
  x-equipes = {demons PROVAL ext}
}
@inproceedings{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 = {10.1145/1292597.1292598},
  publisher = {ACM Press},
  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},
  series = {Lecture Notes in Computer Science},
  volume = {5356},
  pages = {237--254},
  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 = jun,
  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 = jun,
  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 Press},
  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}
}
@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 = {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},
  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 = {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},
  doi = {10.1007/978-3-642-02614-0_10},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-support = {actes},
  topics = {team}
}
@inproceedings{boldo09icalp,
  author = {Sylvie Boldo},
  title = {Floats \& {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},
  hal = {http://hal.inria.fr/inria-00534333},
  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},
  hal = {http://hal.inria.fr/hal-00777577}
}
@inproceedings{KanigFilliatre09wml,
  author = {Johannes Kanig and Jean-Christophe Filli\^atre},
  title = {{Who: A Verifier for Effectful Higher-order Programs}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  address = {Edinburgh, Scotland, UK},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  month = aug,
  year = 2009,
  url = {http://www.lri.fr/~filliatr/ftp/publis/wml09.pdf},
  hal = {http://hal.inria.fr/hal-00777585},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {ML},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  abstract = {We present Who, a tool for verifying effectful higher-order
  functions. It features {\em Effect polymorphism}, higher-order logic
  and the possibility to reason about state in the logic, which enable
  highly modular specifications of generic code. Several small
  examples and a larger case study demonstrate its usefulness. The
  Who~tool is intended to be used as an intermediate language for
  verification tools targeting ML-like programming languages.}
}
@inproceedings{MandelPlateauPouzet-MLworkshop-2009,
  author = {Louis Mandel and Florence Plateau and Marc Pouzet},
  title = {The {ReactiveML} Toplevel (Tool Demonstration)},
  booktitle = {ACM SIGPLAN Workshop on ML},
  address = {Edinburgh, Scotland, UK},
  topics = {team, lri},
  type_publi = {icolcomlec},
  month = aug,
  year = 2009,
  x-type = {article},
  x-support = {actes_aux},
  x-equipes = {demons PROVAL},
  x-cle-support = {ML},
  x-international-audience = {yes},
  x-proceedings = {no},
  x-editorial-board = {yes}
}
@inproceedings{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},
  hal = {http://hal.inria.fr/inria-00534336},
  topics = {team}
}
@inproceedings{tafat11foveoos,
  title = {A Refinement Methodology for Object-Oriented Programs},
  author = {Asma Tafat and Sylvain Boulm\'e and Claude March\'e},
  x-equipes = {demons PROVAL EXT},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-support = {actes},
  x-type = {article},
  x-cle-support = {FOVEOOS},
  topics = {team},
  pages = {153--167},
  hal = {http://hal.inria.fr/inria-00534336},
  crossref = {postfoveoos10}
}
@inproceedings{LescuyerConchon09frocos,
  author = {St{\'e}phane Lescuyer and Sylvain Conchon},
  title = {Improving {Coq} Propositional Reasoning using a Lazy {CNF} Conversion Scheme},
  topics = {team},
  x-support = {actes},
  pages = {287-303},
  doi = {10.1007/978-3-642-04222-5_18},
  crossref = {frocos09}
}
@inproceedings{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},
  hal = {http://hal.inria.fr/inria-00535785},
  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},
  doi = {10.1109/ARITH.2009.36},
  topics = {team},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-pays = {US},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  type_publi = {icolcomlec}
}
@inproceedings{Pouzet-lctes09,
  author = {Paul Caspi and Jean-Louis Cola\c{c}o and L\'eonard G\'erard
                  and Marc Pouzet and Pascal Raymond},
  title = {{Synchronous Objects with Scheduling Policies}:
                   Introducing safe shared memory in {Lustre}},
  year = {2009},
  month = jun,
  address = {Dublin},
  booktitle = {ACM International Conference on
                  Languages, Compilers, and Tools for Embedded Systems
                  (LCTES)},
  url-useless-since-prefix-missing = {lctes09.pdf},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-type = {article},
  x-support = {actes},
  topics = {team}
}
@inproceedings{Pouzet-emsoft09,
  author = {Marc Pouzet and Pascal Raymond},
  title = {Modular Static Scheduling of Synchronous Data-flow
                  Networks: An efficient symbolic representation},
  booktitle = {ACM International Conference on
                  Embedded Software (EMSOFT'09)},
  address = {Grenoble, France},
  month = {October},
  x-proceedings = {yes},
  x-international-audience = {yes},
  year = 2009,
  url-useless-since-prefix-missing = {emsoft09.pdf},
  x-type = {article},
  x-support = {actes},
  topics = {team}
}
@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},
  hal = {http://hal.inria.fr/inria-00450789/},
  doi = {10.1007/978-3-642-14052-5_12/},
  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}
}
@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{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},
  hal = {http://hal.inria.fr/inria-00535640},
  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 = {Manuel Barbosa and Jean-Christophe Filli\^atre and Jorge Sousa Pinto and B\'arbara 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 = jun,
  url = {http://proval.lri.fr/publications/dross11tap.pdf},
  hal = {http://hal.inria.fr/hal-00777683},
  topics = {team},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-equipes = {demons PROVAL ext},
  x-cle-support = {TAP},
  abstract = {
  For critical software development, containers such as lists, vectors, sets or
  maps are an attractive alternative to ad-hoc data structures based on
  pointers.
  As standards like DO-178C put formal verification and testing on an equal
  footing, it is important to give users the ability to apply both to the
  verification of code using containers.
  In this paper,
  we present a definition of containers whose aim is to facilitate their
  use in certified software, using modern proof technology and novel
  specification languages. Correct usage of containers and user-provided
  correctness properties can be checked either by execution during testing
  or by formal proof with an automatic prover.
  We present a formal semantics for containers and an axiomatization of this
  semantics targeted at automatic provers. We have proved in Coq that the
  formal semantics is consistent and that the axiomatization thereof is
  correct.}
}
@inproceedings{filliatre11tfp,
  author = {Jean-Christophe Filli\^atre and Krishnamani Kalyanasundaram},
  title = {Functory: A Distributed Computing Library for {Objective Caml}},
  booktitle = {Trends in Functional Programming},
  year = 2011,
  series = {Lecture Notes in Computer Science},
  volume = {7193},
  pages = {65--81},
  topics = {team},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {TFP},
  x-equipes = {demons PROVAL},
  address = {Madrid, Spain},
  month = {May},
  abstract = {We present Functory, a distributed computing library for
  Objective Caml. The main features of this library
  include (1) a polymorphic API, (2) several implementations to
  adapt to different deployment scenarios such as sequential,
  multi-core or network, and (3) a reliable fault-tolerance mechanism.
  This paper describes the motivation behind this work, as well as
  the design and implementation of the library. It also demonstrates
  the potential of the library using realistic experiments.},
  url = {https://www.lri.fr/~filliatr/publis/tfp11.pdf}
}
@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,
  hal = {http://hal.inria.fr/hal-00790310},
  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},
  keywords = {Why3},
  abstract = {Why3 is the next generation of the
  Why software verification platform.
  Why3 clearly separates the purely logical
  specification part from generation of verification conditions for programs.
  This article focuses on the former part.
  Why3 comes with a new enhanced language of
  logical specification. It features a rich library of
  proof task transformations that can be chained to produce a suitable
  input for a large set of theorem provers, including SMT solvers,
  TPTP provers, as well as interactive proof assistants.}
}
@inproceedings{mandel11fmcad,
  author = {Louis Mandel and Florence Plateau and Marc Pouzet},
  title = {Static Scheduling of Latency Insensitive Designs with {Lucy-n}},
  booktitle = {Formal Methods in Computer Aided Design ({FMCAD 2011})},
  year = 2011,
  month = oct,
  address = {Austin, TX, USA},
  hal = {http://hal.inria.fr/hal-00654843},
  url = {http://www.lri.fr/~mandel/papiers/MandelPlateauPouzet-FMCAD-2011.pdf},
  webpage = {http://www.lri.fr/~mandel/lucy-n/fmcad11/},
  abstract = {Lucy-n is a dataflow programming language similar to Lustre
  extended with a buffer operator. This language is based on the
  n-synchronous model which was initially introduced for programming
  multimedia streaming applications. In this article, we show that
  Lucy-n is also applicable to model Latency Insensitive
  Designs~(LID). In order to model relay stations, we have to
  introduce a delay operator. Thanks to this new operator, a LID can be
  described by a Lucy-n program. Then, the Lucy-n compiler
  automatically provides static schedules for computation nodes and
  buffer sizes needed in the shell wrappers.},
  topics = {team},
  x-teams = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {FMCAD},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{BolMel11,
  author = {Sylvie Boldo and Guillaume Melquiond},
  title = {{Flocq}: A Unified Library for Proving Floating-point Algorithms in {Coq}},
  booktitle = {Proceedings of the 20th IEEE Symposium on Computer Arithmetic},
  editor = {Elisardo Antelo and David Hough and Paolo Ienne},
  address = {T{\"u}bingen, Germany},
  year = {2011},
  pages = {243--252},
  doi = {10.1109/ARITH.2011.40},
  hal = {http://hal.archives-ouvertes.fr/inria-00534854/},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ARITH},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{nguyen11cpp,
  author = {Thi Minh Tuyen Nguyen and Claude March\'e},
  title = {Hardware-Dependent Proofs of Numerical Programs},
  crossref = {cpp2011},
  pages = {314--329},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-support = {actes},
  x-cle-support = {CPP},
  x-type = {article},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  hal = {http://hal.inria.fr/hal-00772508}
}
@inproceedings{BobotPaskevich2011frocos,
  author = {Fran\c{c}ois Bobot and Andrei Paskevich},
  title = {{Expressing Polymorphic Types in a Many-Sorted Language}},
  pages = {87--102},
  topics = {team},
  x-type = {article},
  x-support = {actes},
  x-equipes = {demons PROVAL},
  x-cle-support = {FROCOS},
  url = {http://proval.lri.fr/publications/bobot11frocos.pdf},
  crossref = {frocos11}
}
@inproceedings{herms12vstte,
  title = {A Certified Multi-prover Verification Condition Generator},
  author = {Paolo Herms and Claude March{\'e} and Benjamin Monate},
  crossref = {vstte12},
  hal = {http://hal.inria.fr/hal-00639977},
  pages = {2--17},
  x-equipes = {demons PROVAL ext},
  url = {http://proval.lri.fr/publications/herms12vstte.pdf},
  topics = {team}
}
@inproceedings{filliatre12vstte,
  author = {Jean-Christophe Filli\^atre},
  title = {Verifying Two Lines of {C} with {Why3}: an Exercise in Program Verification},
  crossref = {vstte12},
  pages = {83--97},
  x-equipes = {demons PROVAL},
  topics = {team},
  keywords = {Why3},
  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,
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-support = {article},
  x-cle-support = {ITProving},
  x-type = {article},
  series = {Lecture Notes in Computer Science},
  volume = {7406},
  pdf = {http://hal.inria.fr/hal-00682398/PDF/techreport.pdf},
  hal = {http://hal.inria.fr/hal-00682398},
  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},
  volume = {7316},
  pages = {238--251},
  year = 2012,
  address = {Pisa, Italy},
  month = jun,
  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},
  x-type = {article},
  x-equipes = {demons PROVAL ext},
  topics = {team},
  hal = {http://hal.inria.fr/hal-00789525}
}
@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},
  x-cle-support = {APA},
  address = {Tallinn, Estonia}
}
@inproceedings{filliatre12boogie,
  author = {Jean-Christophe Filli\^atre},
  title = {{Combining Interactive and Automated Theorem Proving
using Why3 (invited tutorial)}},
  booktitle = {{Second International Workshop on Intermediate Verification Languages (BOOGIE 2012)}},
  editor = {Zvonimir Rakamari\'c},
  month = {July},
  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},
  x-cle-support = {BOOGIE},
  address = {Berkeley, California, USA}
}
@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},
  hal = {http://hal.archives-ouvertes.fr/hal-00799272},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-equipes = {demons PROVAL Fortesse ext},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CAV},
  editor = {Madhusudan Parthasarathy and Sanjit A. Seshia},
  series = {Lecture Notes in Computer Science},
  volume = 7358,
  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},
  hal = {http://hal.inria.fr/hal-00687640},
  doi = {10.1007/978-3-642-31365-3_8},
  topics = {team},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-equipes = {demons PROVAL ext},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {IJCAR},
  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 = jun,
  year = 2012,
  hal = {http://hal.inria.fr/hal-00798777},
  editor = {Vladimir Klebanov and Sarah Grebing},
  publisher = {EasyChair},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {no},
  x-equipes = {demons PROVAL ext},
  x-support = {actes_aux},
  x-cle-support = {COMPARE},
  x-type = {article},
  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},
  x-international-audience = {yes},
  x-proceedings = {no},
  x-equipes = {demons PROVAL ext},
  x-support = {rapport},
  x-cle-support = {INFORUM},
  x-type = {article},
  topics = {team},
  keywords = {Why3},
  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},
  url = {http://inforum.org.pt/INForum2012/docs/20120013.pdf}
}
@inproceedings{bobot12icfem,
  hal = {http://hal.inria.fr/hal-00825088},
  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,
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-equipes = {demons PROVAL},
  x-support = {article},
  x-cle-support = {ICFEM},
  x-type = {actes},
  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 Second International Conference on Certified Programs and Proofs},
  pages = {289--304},
  year = {2012},
  editor = {Chris Hawblitzel and Dale Miller},
  volume = {7679},
  optnumber = {},
  series = {Lecture Notes in Computer Science},
  address = {Kyoto, Japan},
  month = dec,
  optorganization = {},
  optpublisher = {},
  optnote = {},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-equipes = {demons PROVAL},
  x-support = {actes},
  x-cle-support = {CPP},
  x-type = {article},
  hal = {http://hal.inria.fr/hal-00712938},
  doi = {10.1007/978-3-642-35308-6_22},
  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},
  pages = {12--21},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-cle-support = {SMT},
  x-type = {article},
  crossref = {smt2012},
  topics = {team}
}
@inproceedings{dross12smt,
  author = {Claire Dross and Sylvain Conchon and Johannes Kanig and Andrei Paskevich},
  title = {Reasoning with Triggers},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  x-cle-support = {SMT},
  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},
  hal = {http://hal.inria.fr/hal-00726631},
  x-equipes = {demons PROVAL ext},
  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},
  doi = {10.4230/LIPIcs.RTA.2012.133},
  hal = {http://hal.archives-ouvertes.fr/hal-00743284},
  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},
  hal = {http://hal.archives-ouvertes.fr/hal-00797956},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  crossref = {popl13}
}
@inproceedings{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}
}
@inproceedings{marche13jfla,
  author = {Claude March\'e and Asma Tafat},
  title = {Calcul de plus faible pr\'econdition, revisité en {Why3}},
  crossref = {jfla13},
  topics = {team},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  hal = {http://hal.inria.fr/hal-00778791}
}
@inproceedings{conchon13jfla,
  author = {Sylvain Conchon and Alain Mebsout and Fatiha Za\"{\i}di},
  title = {V\'erification de syst\`emes param\'etr\'es avec {Cubicle}},
  crossref = {jfla13},
  topics = {team},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL Fortesse},
  x-type = {article},
  x-support = {actes},
  hal = {http://hal.inria.fr/hal-00778832}
}
@inproceedings{filliatre13jfla,
  author = {Jean-Christophe Filli\^atre and R\'emy El Siba\"{\i}e},
  title = {{Combine} : une biblioth\`eque {OCaml} pour la combinatoire},
  crossref = {jfla13},
  topics = {team},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL ext},
  x-type = {article},
  x-support = {actes},
  note = {\url{http://www.lri.fr/~filliatr/combine/}},
  hal = {http://hal.inria.fr/hal-00779431},
  url = {http://www.lri.fr/~filliatr/pub/jfla-2013.pdf}
}
@inproceedings{mandel13jfla,
  author = {Louis Mandel and C{\'e}dric Pasteur},
  title = {R{\'e}activit{\'e} des syst{\`e}mes coop{\'e}ratifs : le cas de {ReactiveML}},
  crossref = {jfla13},
  topics = {team},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL ext},
  x-type = {article},
  x-support = {actes},
  note = {\url{http://rml.lri.fr/jfla13}},
  hal = {http://hal.inria.fr/hal-00779789},
  url = {http://www.lri.fr/~mandel/publications/MandelPasteur-JFLA-2013.pdf},
  abstract = {La concurrence coop{\'e}rative est un mod{\`e}le de programmation tr{\`e}s
r{\'e}pandu. On peut par exemple l'utiliser en OCaml {\`a} travers des
biblioth{\`e}ques comme Lwt, Async ou Equeue. Il a de nombreux avantages
tels que l'absence de courses critiques et des implantations l{\'e}g{\`e}res
et efficaces.  N{\'e}anmoins, un des inconv{\'e}nients majeurs de ce mod{\`e}le
est qu'il d{\'e}pend de la discipline du programmeur pour garantir que le
syst{\`e}me est r{\'e}actif : un processus peut emp{\^e}cher les autres de
s'ex{\'e}cuter.

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

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

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

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

Our work is applied to the ReactiveML language, which extends ML with synchronous language constructs. We present an operational semantics for the extended language and a type system that ensures the soundness of programs.}
}
@inproceedings{mandel12cp,
  author = {Vijay Saraswat and David Cunningham and Liana Hadarean and Louis Mandel and Avraham Shinnar and Olivier Tardieu},
  title = {Constrained Types - Future Directions},
  booktitle = {18th International Conference on Principles and Practice of Constraint Programming},
  year = 2012,
  month = oct,
  address = {Qu{\'e}bec City, Canada},
  note = {Position Paper},
  url = {http://www.lri.fr/~mandel/publications/SaraswatCunninghamHadareanMandelShinnarTardieu-CP-2012.pdf},
  abstract = {The use of constraints in types is quite natural. Yet, integrating constraint based types into the heart of a modern, statically typed, object-oriented programming language is quite tricky. Over the last five years we have designed and implemented the constrained types framework in the programming language X10. In this paper we review the conceptual design, the practical implementation issues, and the many new questions that are raised. We expect the pursuit of these questions to be a profitable area of future work.},
  topics = {team},
  type_publi = {colloque},
  x-equipes = {demons PROVAL ext},
  hal = {http://hal.inria.fr/hal-00798046}
}
@inproceedings{paskevich13cade,
  hal = {http://hal.inria.fr/hal-00825086},
  author = {Jasmin C. Blanchette and Andrei Paskevich},
  title = {{TFF1}: The {TPTP} typed first-order form with rank-1 polymorphism},
  crossref = {cade13},
  x-equipes = {demons PROVAL},
  x-type = {article},
  topics = {team},
  url = {http://www4.in.tum.de/~blanchet/tff1short.pdf}
}
@inproceedings{boldo13arith,
  author = {Sylvie Boldo},
  title = {How to Compute the Area of a Triangle: a Formal Revisit},
  booktitle = {Proceedings of the 21th IEEE Symposium on Computer Arithmetic},
  address = {Austin, Texas, USA},
  year = {2013},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ARITH},
  x-international-audience = {yes},
  x-proceedings = {yes},
  hal = {http://hal.inria.fr/hal-00790071}
}
@inproceedings{bolmel13arith,
  author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond, Guillaume},
  title = {A Formally-Verified {C} Compiler Supporting Floating-Point Arithmetic},
  booktitle = {Proceedings of the 21th IEEE Symposium on Computer Arithmetic},
  address = {Austin, Texas, USA},
  year = {2013},
  topics = {team},
  x-equipes = {demons PROVAL ext},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ARITH},
  x-international-audience = {yes},
  x-proceedings = {yes},
  hal = {http://hal.inria.fr/hal-00743090}
}
@inproceedings{filliatre13esop,
  author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
  title = {Why3 --- Where Programs Meet Provers},
  booktitle = {Proceedings of the 22nd European Symposium on Programming},
  month = mar,
  year = 2013,
  volume = {7792},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Matthias Felleisen and Philippa Gardner},
  pages = {125--128},
  hal = {http://hal.inria.fr/hal-00789533},
  topics = {team,lri},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ESOP},
  x-editorial-board = {yes},
  x-international-audience = {yes}
}
@inproceedings{chargueraud13esop,
  author = {Arthur Chargu{\'e}raud},
  title = {Pretty-Big-Step Semantics},
  booktitle = {Proceedings of the 22nd European Symposium on Programming},
  month = mar,
  year = 2013,
  volume = {7792},
  editor = {Matthias Felleisen and Philippa Gardner},
  pages = {41--60},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  hal = {http://hal.inria.fr/hal-00798227},
  topics = {team,lri},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ESOP},
  x-editorial-board = {yes},
  x-international-audience = {yes}
}
@inproceedings{chargueraud13ppopp,
  author = {Umut A. Acar and Arthur Chargu{\'e}raud and Mike Rainey},
  title = {Scheduling parallel programs by work stealing with private deques},
  booktitle = {Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of parallel programming},
  month = feb,
  year = 2013,
  series = {PPoPP '13},
  pages = {219-228},
  publisher = {ACM Press},
  doi = {10.1145/2442516.2442538},
  hal = {http://hal.inria.fr/hal-00863028},
  topics = {team,lri},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {PPOPP},
  x-editorial-board = {yes},
  x-international-audience = {yes}
}
@inproceedings{filliatre13plmw,
  author = {Jean-Christophe Filli\^atre},
  title = {{Deductive Program Verification}},
  booktitle = {{Programming Languages Mentoring Workshop (PLMW 2013)}},
  editor = {Nate Foster and Philippa Gardner and Alan Schmitt and
 Gareth Smith and Peter Thieman and Tobias Wrigstad},
  month = {January},
  hal = {http://hal.inria.fr/hal-00799190},
  year = 2013,
  topics = {team},
  type_digiteo = {conf_autre},
  type_publi = {colloque},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {no},
  x-invited-conference = {yes},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-support = {actes},
  address = {Rome, Italy}
}
@inproceedings{filliatre13cade,
  author = {Jean-Christophe Filli\^atre},
  title = {One Logic To Use Them All},
  crossref = {cade13},
  pages = {1--20},
  topics = {team,lri},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-invited-conference = {yes},
  hal = {http://hal.inria.fr/hal-00809651/en/}
}
@inproceedings{bobot13vstte,
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
  hal = {http://hal.inria.fr/hal-00875395},
  title = {Preserving User Proofs Across Specification Changes},
  crossref = {vstte13},
  pages = {191--201},
  topics = {team,lri},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{IshMelNak13,
  hal = {http://hal.inria.fr/hal-00806701},
  author = {Daisuke Ishii and Guillaume Melquiond and Shin Nakajima},
  title = {Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus},
  booktitle = {Proceedings of the 10th Conference on Integrated Formal Methods},
  editor = {Einar Broch Johnsen and Luigia Petre},
  address = {Turku, Finland},
  year = {2013},
  pages = {139--153},
  series = {Lecture Notes in Computer Science},
  volume = {7940},
  doi = {10.1007/978-3-642-38613-8_10},
  topics = {team,lri},
  type_publi = {icolcomlec}
}
@inproceedings{kanig12hilt,
  topics = {team},
  author = {Johannes Kanig and Edmond Schonberg and Claire Dross},
  title = {{Hi-Lite}: the convergence of compiler technology and program
               verification},
  pages = {27--34},
  editor = {Ben Brosgol and Jeff Boleng and S. Tucker Taft},
  booktitle = {Proceedings of the 2012 ACM Conference on High Integrity
               Language Technology, HILT '12},
  address = {Boston, USA},
  publisher = {ACM Press},
  year = 2012
}
@inproceedings{clochard14plpv,
  hal = {http://hal.inria.fr/hal-00913431},
  topics = {team},
  author = {Martin Clochard and Claude March\'e and Andrei Paskevich},
  title = {Verified Programs with Binders},
  booktitle = {Programming Languages meets Program Verification (PLPV)},
  year = 2014,
  publisher = {ACM Press},
  type_digiteo = {conf_isbn},
  type_publi = {colloque},
  x-equipes = {demons Toccata},
  x-support = {actes},
  x-cle-support = {PLPV}
}
@inproceedings{castagna14popl,
  hal = {http://hal.archives-ouvertes.fr/hal-00880744},
  topics = {team},
  author = {Giuseppe Castagna and Hyeonseung Im and Serge{\"\i} Lenglet and Kim Nguyen and Luca Padovani and Zhiwu Xu},
  title = {Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation},
  crossref = {popl2014}
}
@inproceedings{castagna15popl,
  hal = {},
  topics = {team},
  author = {Giuseppe Castagna and Kim Nguyen and Zhiwu Xu and Pietro Abate},
  title = {Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction. },
  crossref = {popl2015}
}
@inproceedings{clochard14popl,
  hal = {http://hal.inria.fr/hal-00920955},
  topics = {team},
  author = {M. Clochard and S. Chaudhuri and A. Solar-Lezama},
  title = {Bridging Boolean and Quantitative Synthesis Using Smoothed Proof Search},
  crossref = {popl2014}
}
@inproceedings{bodin14popl,
  hal = {http://hal.inria.fr/hal-00910135},
  topics = {team},
  author = {M. Bodin and A. Chargu{\'e}raud and D. Filaretti and P. Gardner and S. Maffeis and D. Naudziuniene and A. Schmitt and G. Smith},
  title = {A Trusted Mechanised {JavaScript} Specification},
  crossref = {popl2014}
}
@inproceedings{filliatre14cav,
  author = {Jean-Christophe Filli\^atre and L\'eon
            Gondelman and Andrei Paskevich},
  title = {The Spirit of Ghost Code},
  pages = {1--16},
  crossref = {cav2014},
  topics = {team},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes},
  hal_id = {hal-00873187},
  hal = {http://hal.archives-ouvertes.fr/hal-00873187/en/},
  pdf = {http://hal.archives-ouvertes.fr/hal-00873187/PDF/main.pdf},
  abstract = {
  In the context of deductive program verification, ghost code is part
  of the program that is added for the purpose of specification.
  Ghost code must not interfere with regular code, in the sense that
  it can be erased without any observable difference in the program outcome.
  In particular, ghost data cannot participate in regular
  computations and ghost code cannot mutate regular data or diverge.
  The idea exists in the folklore since the early notion of auxiliary
  variables and is implemented in many state-of-the-art program
  verification tools. However, a rigorous definition and treatment of
  ghost code is surprisingly subtle and few formalizations exist.

  In this article, we describe a simple ML-style programming language
  with mutable state and ghost code.  Non-interference is ensured by a
  type system with effects, which allows, notably, the same data types
  and functions to be used in both regular and ghost code.
  We define the procedure of ghost code erasure and we prove its
  safety using bisimulation.
  A similar type system, with numerous extensions which we briefly discuss,
  is implemented in the program verification environment Why3.
  }
}
@inproceedings{delahaye14afadl,
  topics = {team},
  hal_id = {hal-00998094},
  hal = {http://hal.inria.fr/hal-00998094/en/},
  title = {Le projet {BWare} : une plate-forme pour la v{\'e}rification automatique d'obligations de preuve {B}},
  author = {Delahaye, David and March{\'e}, Claude and Mentr{\'e}, David},
  abstract = {Le projet de recherche industrielle BWare (ANR-12-INSE-0010) est financ{\'e} pour 4 ans par le programme \emph{Ing{\'e}nierie Num{\'e}rique \& S{\'e}curit{\'e}} (INS) de l'Agence Nationale de la Recherche (ANR) et a d{\'e}but{\'e} en septembre 2012 (voir le site web du projet : \url{http://bware.lri.fr}). Le consortium du projet BWare associe les partenaires acad{\'e}miques Cedric, LRI, et Inria, ainsi que les partenaires industriels Mitsubishi Electric R\&D Centre Europe (MERCE), ClearSy, et OCamlPro},
  booktitle = {Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels (AFADL)},
  publisher = {EasyChair},
  address = {Paris, France},
  audience = {nationale},
  year = 2014,
  month = jun
}
@inproceedings{delahaye14abz,
  topics = {team},
  crossref = {abz2014},
  hal_id = {hal-00998092},
  hal = {http://hal.inria.fr/hal-00998092/en/},
  title = {The {BWare} Project: Building a Proof Platform for the Automated Verification of {B} Proof Obligations},
  author = {Delahaye, David and Dubois, Catherine and March{\'e}, Claude and Mentr{\'e}, David},
  abstract = { We introduce BWare, an industrial research project
                  that aims to provide a mechanized framework to
                  support the automated veri cation of proof
                  obligations coming from the development of
                  industrial applications using the B method and
                  requiring high integrity. The methodology adopted
                  consists in building a generic verification platform
                  relying on di erent theorem provers, such as rst
                  order provers and SMT (Satisfiability Modulo
                  Theories) solvers. Beyond the multi-tool aspect of
                  our methodology, the originality of this project
                  also resides in the requirement for the veri cation
                  tools to produce proof objects, which are to be
                  checked independently. In this paper, we present
                  some preliminary results of BWare, as well as some
                  current major lines of work},
  language = {Anglais},
  affiliation = {Centre d'Etude et De Recherche en Informatique du Cnam - CEDRIC , TOCCATA - INRIA Saclay - {\^I}le-de-France , Laboratoire de Recherche en Informatique - LRI , Mitsubishi Electric R\&D Centre Europe [France] - MERCE-France},
  pages = {290--293}
}
@inproceedings{conchon14abz,
  topics = {team},
  hal = {https://hal.inria.fr/hal-01093000},
  author = {Sylvain Conchon and Mohamed Iguernelala},
  title = {Tuning the {Alt-Ergo} {SMT} Solver for {B} Proof Obligations},
  pages = {294--297},
  year = 2014,
  crossref = {abz2014},
  doi = {10.1007/978-3-662-43652-3_27}
}
@inproceedings{cfmp14vstte,
  hal = {http://hal.inria.fr/hal-01067197},
  author = {Martin Clochard and Jean-Christophe
  Filli\^atre and Claude March\'e and Andrei Paskevich},
  title = {Formalizing Semantics with an Automatic Program
  Verifier},
  pages = {37--51},
  crossref = {vstte14},
  topics = {team,lri},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{cfp15vstte,
  hal = {http://hal.inria.fr/hal-01162661},
  author = {Martin Clochard and Jean-Christophe
  Filli\^atre and Andrei Paskevich},
  title = {How to avoid proving the absence of integer overflows},
  crossref = {vstte15},
  topics = {team,lri},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{clochard14vstte,
  hal = {http://hal.inria.fr/hal-01067217},
  author = {Martin Clochard},
  title = {Automatically verified implementation of data structures
                  based on {AVL} trees},
  pages = {167--180},
  crossref = {vstte14},
  topics = {team,lri},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{conchon13fmcad,
  topics = {team},
  hal = {http://hal.archives-ouvertes.fr/hal-00924640},
  title = {Invariants for Finite Instances and Beyond},
  author = {Conchon, Sylvain and Goel, Amit and Krsti{\'c}, Sava and Mebsout, Alain and Za{\"\i}di, Fatiha},
  abstract = {Verification of safety properties of concurrent programs with an arbitrary numbers of processes is an old challenge. In particular, complex parameterized protocols like FLASH are still out of the scope of state-of-the-art model checkers. In this paper, we describe a new algorithm, called Brab, that is able to automatically infer invariants strong enough to prove a protocol like FLASH. Brab computes over-approximations of backward reachable states that are checked to be unreachable in a finite instance of the system. These approximations (candidate invariants) are then model checked together with the original safety properties. Completeness of the approach is ensured by a mechanism for backtracking on spurious traces introduced by too coarse approximations.},
  booktitle = {FMCAD},
  pages = {61--68},
  address = {Portland, Oregon, {\'E}tats-Unis},
  audience = {internationale},
  doi = {10.1109/FMCAD.2013.6679392},
  year = 2013,
  month = oct
}
@inproceedings{conchon14jfla,
  hal = {https://hal.inria.fr/hal-01088655},
  topics = {team},
  author = {Sylvain Conchon and David Declerck and Luc Maranget and Alain Mebsout},
  title = {Vérification de programmes {C} concurrents avec {Cubicle} : Enfoncer les barrières},
  crossref = {jfla14}
}
@inproceedings{clochard15jfla,
  hal = {https://hal.inria.fr/hal-01094488},
  topics = {team},
  author = {Martin Clochard and L\'eon Gondelman},
  title = {Double {WP}: vers une preuve automatique d'un compilateur},
  crossref = {jfla15}
}
@inproceedings{acar14esa,
  topics = {team},
  title = {Theory and Practice of Chunked Sequences},
  author = {Acar, Umut A. and Chargu{\'e}raud, Arthur and Rainey, Mike},
  hal = {https://hal.inria.fr/hal-01087245},
  booktitle = {European Symposium on Algorithms},
  address = {Wroclaw, Poland},
  editor = {Schulz, AndreasS. and Wagner, Dorothea},
  publisher = {Springer},
  volume = {Lecture Notes in Computer Science},
  number = 8737,
  pages = {25--36},
  year = 2014,
  month = sep,
  doi = {10.1007/978-3-662-44777-2_3},
  keywords = {Data structure ;  Sequence ;  Chunk ;  Amortization}
}
@inproceedings{lelay15coq,
  topics = {team},
  title = {How to express convergence for analysis in {Coq}},
  author = {Lelay, Catherine},
  hal = {https://hal.archives-ouvertes.fr/hal-01169321},
  booktitle = {The 7th Coq Workshop},
  address = {Sophia Antipolis, France},
  year = 2015,
  month = jun,
  keywords = {Coq proof assistant ;  Analysis ;  Limits ;  Filters ;  Type-Classes ;  Canonical Structures}
}
@inproceedings{lelay14jfla,
  topics = {team},
  title = {{Coq passe le bac}},
  author = {Lelay, Catherine},
  booktitle = {{JFLA - Journ{\'e}es francophones des langages applicatifs}},
  address = {Fr{\'e}jus, France},
  year = {2014},
  month = jan,
  x-proceedings = {no},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-invited-conference = {yes},
  x-scientific-popularization = {no}
}
@inproceedings{pereira16jfla,
  topics = {team},
  author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
  title = {It\'erer avec confiance},
  crossref = {jfla16},
  hal = {https://hal.inria.fr/hal-01240891}
}
@inproceedings{pereira16nfm,
  topics = {team},
  author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
  title = {A Modular Way to Reason About Iteration},
  crossref = {nfm16},
  abstract = { In this paper we present an approach to specify
                  programs performing iterations. The idea is to
                  specify iteration in terms of the nite sequence of
                  the elements enumerated so far, and only those. In
                  particular, we are able to deal with
                  non-deterministic and possibly innite iteration. We
                  show how to cope with the issue of an iteration no
                  longer being consistent with mutable data. We
                  validate our proposal using the deductive verication
                  tool Why3 and two iteration paradigms, namely
                  cursors and higher-order iterators. For each
                  paradigm, we verify several implementations of
                  iterators and client code. This is done in a modular
                  way, i.e., the client code only relies on the
                  specication of the iteration. },
  hal = {https://hal.inria.fr/hal-01281759}
}
@inproceedings{fumex16nfm,
  topics = {team},
  author = {Fumex, Cl\'ement and Dross, Claire and Gerlach, Jens and March\'e, Claude},
  title = {Specification and Proof of High-Level Functional Properties of Bit-Level Programs},
  crossref = {nfm16},
  hal = {https://hal.inria.fr/hal-01314876}
}
@inproceedings{hauzar16sefm,
  topics = {team},
  author = {Hauzar, David and March\'e, Claude and Moy, Yannick},
  title = {Counterexamples from Proof Failures in {SPARK}},
  booktitle = {Software Engineering and Formal Methods},
  year = 2016,
  pages = {215--233},
  hal = {https://hal.inria.fr/hal-01314885}
}
@inproceedings{filliatre16,
  topics = {team},
  author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
  title = {Producing All Ideals of a Forest, Formally (Verification Pearl)},
  crossref = {vstte16},
  hal = {https://hal.inria.fr/hal-01316859}
}
@inproceedings{clochard16,
  topics = {team},
  author = {Martin Clochard and L\'eon Gondelman and M\'ario Pereira},
  title = {The {Matrix} Reproved},
  crossref = {vstte16},
  hal = {https://hal.inria.fr/hal-01316902}
}
@inproceedings{kosmatov16isola,
  topics = {team},
  title = {Static versus Dynamic Verification in {Why3}, {Frama-C} and {SPARK 2014}},
  author = {Kosmatov, Nikolai and March{\'e}, Claude and Moy, Yannick and Signoles, Julien},
  hal = {https://hal.inria.fr/hal-01344110},
  booktitle = {7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  year = 2016,
  pages = {461--478},
  month = oct
}
@inproceedings{boldo16nsv,
  title = {{Computing a correct and tight rounding error bound using rounding-to-nearest}},
  author = {Boldo, Sylvie},
  hal = {https://hal.inria.fr/hal-01377152},
  booktitle = {{9th International Workshop on Numerical Software Verification}},
  address = {Toronto, Canada},
  year = {2016},
  month = jul,
  pdf = {https://hal.inria.fr/hal-01377152/file/article.pdf},
  topics = {team}
}
@inproceedings{boldo16hccv,
  title = {{Iterators: where folds fail}},
  author = {Boldo, Sylvie},
  hal = {https://hal.inria.fr/hal-01377155},
  booktitle = {{Workshop on High-Consequence Control Verification}},
  address = {Toronto, Canada},
  year = {2016},
  month = jul,
  pdf = {https://hal.inria.fr/hal-01377155/file/abstract.pdf},
  topics = {team}
}
@inproceedings{chargueraud:hal-01245872,
  topics = {team},
  title = {{Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation}},
  author = {Chargu\'eraud, Arthur and Pottier, Fran\c{c}ois},
  booktitle = {{6th International Conference on Interactive Theorem Proving (ITP)}},
  address = {Nanjing, China},
  year = 2015,
  month = aug,
  doi = {10.1007/978-3-319-22102-1\_9},
  hal = {https://hal.inria.fr/hal-01245872},
  pdf = {https://hal.inria.fr/hal-01245872/document},
  hal_id = {hal-01245872},
  hal_version = {v1},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@inproceedings{acar:hal-01245837,
  topics = {team},
  title = {{A Work-Efficient Algorithm for Parallel Unordered Depth-First Search}},
  author = {Acar, Umut A. and Chargu\'eraud, Arthur and Rainey, Mike},
  booktitle = {{Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis}},
  address = {Austin, Texas, United States},
  year = {2015},
  month = nov,
  doi = {10.1145/2807591.2807651},
  hal = {https://hal.inria.fr/hal-01245837},
  pdf = {https://hal.inria.fr/hal-01245837/document},
  hal_id = {hal-01245837},
  hal_version = {v1},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@inproceedings{boldo:hal-01391578,
  topics = {team},
  title = {{A Coq Formal Proof of the Lax-Milgram theorem}},
  author = {Boldo, Sylvie and Cl{\'e}ment, Fran{\c c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
  hal = {https://hal.inria.fr/hal-01391578},
  booktitle = {{6th ACM SIGPLAN Conference on Certified Programs and Proofs}},
  address = {Paris, France},
  year = {2017},
  month = jan,
  keywords = {Lax-Milgram theorem ; formal proof ; functional analysis ; finite element method ; Coq},
  hal_id = {hal-01391578},
  hal_version = {v1}
}
@inproceedings{chargueraud:hal-01245865,
  topics = {team},
  title = {{Higher-Order Representation Predicates in Separation Logic}},
  author = {Chargu{\'e}raud, Arthur},
  hal = {https://hal.inria.fr/hal-01245865},
  booktitle = {{Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs}},
  address = {Saint Petersburg, Florida, United States},
  year = {2016},
  month = jan,
  hal_id = {hal-01245865},
  hal_version = {v1}
}
@inproceedings{mahboubi16itp,
  topics = {team},
  title = {{Formally Verified Approximations of Definite Integrals}},
  author = {Mahboubi, Assia and Melquiond, Guillaume and Sibut-Pinote, Thomas},
  hal = {https://hal.inria.fr/hal-01289616},
  booktitle = {{Interactive Theorem Proving}},
  address = {Nancy, France},
  editor = {Jasmin Christian Blanchette and Stephan Merz},
  series = {Lecture Notes in Computer Science},
  volume = {9807},
  year = {2016},
  month = aug,
  doi = {10.1007/978-3-319-43144-4\_17},
  pdf = {https://hal.inria.fr/hal-01289616/file/main.pdf},
  hal_id = {hal-01289616},
  hal_version = {v2}
}
@inproceedings{chen17jfla,
  topics = {team},
  author = {Ran Chen and Jean-Jacques L\'evy},
  title = {Une preuve formelle de l'algorithme de {Tarjan-1972} pour trouver les composantes fortement connexes dans un graphe},
  crossref = {jfla17},
  hal = {https://hal.inria.fr/hal-01405424}
}
@inproceedings{clochard17jfla,
  topics = {team},
  title = {{Preuves taill{\'e}es en biseau}},
  author = {Clochard, Martin},
  hal = {https://hal.inria.fr/hal-01404935},
  crossref = {jfla17}
}
@inproceedings{pereira17jfla,
  topics = {team},
  title = {{D{\'e}fonctionnaliser pour prouver}},
  author = {Pereira, M{\'a}rio},
  hal = {https://hal.inria.fr/hal-01378068},
  crossref = {jfla17}
}
@inproceedings{rieuhelft17jfla,
  topics = {team},
  title = {Result graphs for an abstract interpretation-based static analyzer},
  author = {Rapha{\"e}l Rieu-Helft and Pascal Cuoq},
  crossref = {jfla17}
}
@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{popl2014,
  title = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year = 2014,
  booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  address = {San Diego, USA},
  month = jan,
  publisher = {ACM Press}
}
@proceedings{popl2015,
  title = {Proceedings of the 42st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year = 2015,
  booktitle = {Proceedings of the 42st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  address = {Mumbai, India},
  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{cav2014,
  editor = {Armin Biere and Roderick Bloem},
  title = {Computer Aided Verification},
  booktitle = {26th International Conference on Computer Aided Verification},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 8859,
  address = {Vienna, Austria},
  month = jul,
  year = 2014
}
@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},
  x-cle-support = {JFLA}
}
@proceedings{jfla13,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2013,
  booktitle = {Vingt-quatri\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = feb,
  address = {Aussois, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@proceedings{jfla14,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2014,
  booktitle = {Vingt-cinqui\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Fr\'ejus, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@proceedings{jfla15,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2015,
  booktitle = {Vingt-sixi\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Val d'Ajol, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@proceedings{jfla16,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2016,
  booktitle = {Vingt-septi\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Saint-Malo, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@proceedings{jfla17,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2017,
  booktitle = {Vingt-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Gourette, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@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{esop2014,
  title = {23rd European Symposium on Programming (ESOP)},
  year = 2014,
  booktitle = {ESOP},
  editor = {Zhong Shao},
  series = {Lecture Notes in Computer Science},
  address = {Grenoble},
  month = apr,
  publisher = {Springer}
}
@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,
  hal = {http://hal.inria.fr/hal-00772519},
  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},
  volume = 7421,
  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 = {Verified Software: Theories, Tools, Experiments (4th International Conference VSTTE)},
  month = jan,
  year = 2012,
  address = {Philadelphia, USA},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {VSTTE},
  editor = {Rajeev Joshi and Peter M{\"u}ller and Andreas Podelski},
  series = {Lecture Notes in Computer Science},
  volume = 7152,
  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 = {LORIA},
  url = {http://smt2012.loria.fr/},
  year = 2012,
  x-international-audience = {yes},
  x-proceedings = {no},
  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},
  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},
  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}
}
@proceedings{cade13,
  title = {24th International Conference on Automated Deduction},
  booktitle = {24th International Conference on Automated Deduction (CADE-24)},
  address = {Lake Placid, USA},
  month = {June},
  year = 2013,
  series = {Lecture Notes in Artificial Intelligence},
  volume = 7898,
  publisher = {Springer}
}
@proceedings{vstte13,
  booktitle = {Verified Software: Theories, Tools, Experiments (5th International Conference VSTTE)},
  month = may,
  year = 2013,
  address = {Atherton, USA},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {VSTTE},
  editor = {Ernie Cohen and Andrey Rybalchenko},
  series = {Lecture Notes in Computer Science},
  volume = {8164},
  publisher = {Springer}
}
@proceedings{vstte14,
  booktitle = {6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
  month = jul,
  year = 2014,
  address = {Vienna, Austria},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {VSTTE},
  editor = {Dimitra Giannakopoulou and Daniel Kroening},
  series = {Lecture Notes in Computer Science},
  volume = 8471,
  publisher = {Springer}
}
@proceedings{vstte15,
  booktitle = {7th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
  month = jul,
  year = 2015,
  address = {San Francisco, California, USA},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {VSTTE},
  editor = {Arie Gurfinkel and Sanjit A. Seshia},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer}
}
@proceedings{vstte16,
  booktitle = {8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
  month = jul,
  year = 2016,
  address = {Toronto, Canada},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {VSTTE},
  editor = {Sandrine Blazy and Marsha Chechik},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer}
}
@proceedings{abz2014,
  booktitle = {Abstract State Machines, Alloy, B, VDM, and Z (ABZ)},
  publisher = {Springer},
  address = {Toulouse, France},
  volume = 8477,
  series = {Lecture Notes in Computer Science},
  audience = {internationale},
  year = 2014,
  month = jun
}
@proceedings{nfm16,
  booktitle = {8th NASA Formal Methods Symposium},
  address = {Minneapolis, MN, USA},
  audience = {internationale},
  year = 2016,
  month = jun,
  series = {Lecture Notes in Computer Science},
  volume = {9690},
  publisher = {Springer}
}