2012-conference.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc 2012-conference.cite -ob 2012-conference.bib -c 'year = 2012 and topics : "team" and $type="inproceedings"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@inproceedings{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{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{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 = {https://usr.lmf.cnrs.fr/~jcf/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 = {https://usr.lmf.cnrs.fr/~jcf/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://hal.inria.fr/hal-00825088}
}
@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{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{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
}
@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},
  year = {2012},
  volume = {15},
  editor = {Ashish Tiwari},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address = {Nagoya, Japan},
  isbn = {978-3-939897-38-5}
}
@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{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{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{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}
}