paskevich.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -oc paskevich.cite -ob paskevich.bib -c 'author : "paskevich" and topics : "team"' /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{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}
}
@techreport{paskevich09rr,
  author = {Andrei Paskevich},
  title = {Algebraic types and pattern matching in the logical language of the {Why} verification platform},
  institution = {INRIA},
  year = 2009,
  topics = {team},
  hal = {http://hal.inria.fr/inria-00439232},
  note = {\url{http://hal.inria.fr/inria-00439232}},
  number = 7128
}
@techreport{paskevich10rr,
  author = {Andrei Paskevich},
  title = {Algebraic types and pattern matching in the logical language of the {Why} verification platform (version 2)},
  institution = {INRIA},
  year = 2010,
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  hal = {http://hal.inria.fr/inria-00439232/en/},
  note = {\url{http://hal.inria.fr/inria-00439232/en/}},
  number = 7128
}
@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}
}
@misc{BobotPaskevich2011,
  author = {Fran\c{c}ois Bobot and Andrei Paskevich},
  title = {{Expressing Polymorphic Types in a Many-Sorted Language}},
  year = 2011,
  topics = {team},
  note = {Preliminary report. \url{http://hal.inria.fr/inria-00591414/}}
}
@manual{bobot11why3,
  title = {The Why3 platform},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
  organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
  edition = {version 0.64},
  month = feb,
  year = 2011,
  topics = {team},
  keywords = {Why3},
  note = {\url{http://why3.lri.fr/}}
}
@manual{why3manual071,
  title = {The Why3 platform, version 0.71},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Andrei Paskevich},
  organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
  edition = {version 0.71},
  month = oct,
  year = 2011,
  topics = {team},
  keywords = {Why3},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  note = {\url{https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf}}
}
@manual{why3manual072,
  title = {The Why3 platform, version 0.72},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
  organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
  edition = {version 0.72},
  month = may,
  year = 2012,
  topics = {team},
  keywords = {Why3},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  pdf = {https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf},
  rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf}}
}
@manual{why3manual073,
  title = {The Why3 platform, version 0.73},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
  organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
  edition = {version 0.73},
  month = jul,
  year = 2012,
  topics = {team},
  keywords = {Why3},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  pdf = {https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf},
  rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf}}
}
@manual{why3manual080,
  title = {The Why3 platform, version 0.80},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
  organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
  edition = {version 0.80},
  month = oct,
  year = 2012,
  topics = {team},
  keywords = {Why3},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  pdf = {https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf},
  note = {\url{https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf}},
  rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf}}
}
@manual{why3manual081,
  title = {The Why3 platform, version 0.81},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
  organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
  edition = {version 0.81},
  month = mar,
  year = 2013,
  topics = {team},
  keywords = {Why3},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons TOCCATA},
  pdf = {http://why3.lri.fr/download/manual-0.81.pdf},
  note = {\url{http://why3.lri.fr/download/manual-0.81.pdf}},
  hal = {http://hal.inria.fr/hal-00822856/}
}
@manual{why3manual082,
  title = {The Why3 platform, version 0.82},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
  organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
  edition = {version 0.82},
  month = dec,
  year = 2013,
  topics = {team},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons TOCCATA},
  pdf = {http://why3.lri.fr/download/manual-0.82.pdf},
  note = {\url{http://why3.lri.fr/download/manual-0.82.pdf}},
  hal = {}
}
@manual{why3manual0861,
  title = {The Why3 platform, version 0.86.1},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
  organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
  edition = {version 0.86.1},
  month = may,
  year = 2015,
  topics = {team},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons TOCCATA},
  pdf = {http://why3.lri.fr/download/manual-0.86.1.pdf},
  note = {\url{http://why3.lri.fr/download/manual-0.86.1.pdf}},
  hal = {}
}
@inproceedings{boogie11why3,
  topics = {team},
  hal = {http://hal.inria.fr/hal-00790310},
  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},
  booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages},
  year = 2011,
  address = {Wroc\l{}aw, Poland},
  month = {August},
  pages = {53--64},
  note = {\url{https://hal.inria.fr/hal-00790310}},
  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{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}
}
@techreport{dross12rr,
  title = {Reasoning with Triggers},
  author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes
                  and Paskevich, Andrei},
  abstract = {SMT solvers can decide the satisfiability of ground
                  formulas modulo a combination of built-in
                  theories. Adding a built-in theory to a given SMT
                  solver is a complex and time consuming task that
                  requires internal knowledge of the solver. However,
                  many theories can be easily expressed using
                  first-order formulas. Unfortunately, since universal
                  quantifiers are not handled in a complete way by SMT
                  solvers, these axiomatics cannot be used as decision
                  procedures. In this paper, we show how to extend a
                  generic SMT solver to accept a custom theory
                  description and behave as a decision procedure for
                  that theory, provided that the described theory is
                  complete and terminating in a precise sense. The
                  description language consists of first-order axioms
                  with triggers, an instantiation mechanism that is
                  found in many SMT solvers. This mechanism, which
                  usually lacks a clear semantics in existing
                  languages and tools, is rigorously defined here;
                  this definition can be used to prove completeness
                  and termination of the theory. We demonstrate on two
                  examples, how such proofs can be achieved in our
                  formalism.},
  keywords = {Quantifiers, Triggers, SMT Solvers, Theories},
  language = {English},
  affiliation = {PROVAL - INRIA Saclay - Ile de France , Laboratoire de Recherche en Informatique - LRI},
  pages = 29,
  type = {Research Report},
  institution = {INRIA},
  number = {RR-7986},
  year = 2012,
  month = jun,
  x-equipes = {demons PROVAL ext},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  hal = {http://hal.inria.fr/hal-00703207},
  pdf = {http://hal.inria.fr/hal-00703207/PDF/RR-7986.pdf}
}
@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{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}
}
@techreport{blanchette12tr,
  author = {Jasmin C. Blanchette and Andrei Paskevich},
  title = {{TFF1}: The {TPTP} typed first-order form with rank-1 polymorphism},
  institution = {Tech. Univ. Munich},
  year = 2012,
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  url = {http://www21.in.tum.de/~blanchet/tff1spec.pdf},
  note = {\url{http://www21.in.tum.de/~blanchet/tff1spec.pdf}}
}
@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{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{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{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}
}
@unpublished{dross13,
  topics = {team},
  hal = {http://hal.inria.fr/hal-00915931},
  title = {Adding Decision Procedures to {SMT} Solvers using Axioms with Triggers},
  author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes and Paskevich, Andrei},
  abstract = {SMT solvers are efficient tools to decide the
                  satisfiability of ground formulas, including a
                  number of built-in theories such as congruence,
                  linear arithmetic, arrays, and bit-vectors. Adding a
                  theory to that list requires delving into the
                  implementation details of a given SMT solver, and is
                  done mainly by the developers of the solver
                  itself. For many useful theories, one can
                  alternatively provide a first-order
                  axiomatization. However, in the presence of
                  quantifiers, SMT solvers are incomplete and exhibit
                  unpredictable behavior. Consequently, this approach
                  can not provide us with a complete and terminating
                  treatment of the theory of interest. In this paper,
                  we propose a framework to solve this problem, based
                  on the notion of instantiation patterns, also known
                  as triggers. Triggers are annotations that suggest
                  instances which are more likely to be useful in
                  proof search. They are implemented in all SMT
                  solvers that handle first-order logic and are
                  included in the SMT-LIB format. In our framework,
                  the user provides a theory axiomatization with
                  triggers, along with a proof of completeness and
                  termination properties of this axiomatization, and
                  obtains a sound, complete, and terminating solver
                  for her theory in return. We describe and prove a
                  corresponding extension of the traditional Abstract
                  DPLL Modulo Theory framework. Implementing this
                  mechanism in a given SMT solver requires a one-time
                  development effort. We believe that this effort is
                  not greater than that of adding a single decision
                  procedure to the same SMT solver. We have
                  implemented the proposed extension in the Alt-Ergo
                  prover and we discuss some implementation details in
                  the paper. To show that our framework can handle
                  complex theories, we prove completeness and
                  termination of a feature-rich axiomatization of
                  doubly-linked lists. Our tests show that our
                  approach results in a better performance of the
                  solver on goals that stem from the verification of
                  programs manipulating doubly-linked lists.},
  language = {Anglais},
  affiliation = {TOCCATA - INRIA Saclay - {\^I}le-de-France , Laboratoire de Recherche en Informatique - LRI , AdaCore SAS - AdaCore SAS},
  year = 2013,
  pdf = {http://hal.inria.fr/hal-00915931/PDF/dross-article.pdf},
  note = {Submitted}
}
@article{dross16jar,
  topics = {team},
  hal = {https://hal.archives-ouvertes.fr/hal-01221066},
  title = {Adding Decision Procedures to {SMT} Solvers using Axioms with Triggers},
  author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes and Paskevich, Andrei},
  abstract = {SMT solvers are efficient tools to decide the
                  satisfiability of ground formulas, including a
                  number of built-in theories such as congruence,
                  linear arithmetic, arrays, and bit-vectors. Adding a
                  theory to that list requires delving into the
                  implementation details of a given SMT solver, and is
                  done mainly by the developers of the solver
                  itself. For many useful theories, one can
                  alternatively provide a first-order
                  axiomatization. However, in the presence of
                  quantifiers, SMT solvers are incomplete and exhibit
                  unpredictable behavior. Consequently, this approach
                  can not provide us with a complete and terminating
                  treatment of the theory of interest. In this paper,
                  we propose a framework to solve this problem, based
                  on the notion of instantiation patterns, also known
                  as triggers. Triggers are annotations that suggest
                  instances which are more likely to be useful in
                  proof search. They are implemented in all SMT
                  solvers that handle first-order logic and are
                  included in the SMT-LIB format. In our framework,
                  the user provides a theory axiomatization with
                  triggers, along with a proof of completeness and
                  termination properties of this axiomatization, and
                  obtains a sound, complete, and terminating solver
                  for her theory in return. We describe and prove a
                  corresponding extension of the traditional Abstract
                  DPLL Modulo Theory framework. Implementing this
                  mechanism in a given SMT solver requires a one-time
                  development effort. We believe that this effort is
                  not greater than that of adding a single decision
                  procedure to the same SMT solver. We have
                  implemented the proposed extension in the Alt-Ergo
                  prover and we discuss some implementation details in
                  the paper. To show that our framework can handle
                  complex theories, we prove completeness and
                  termination of a feature-rich axiomatization of
                  doubly-linked lists. Our tests show that our
                  approach results in a better performance of the
                  solver on goals that stem from the verification of
                  programs manipulating doubly-linked lists.},
  year = 2016,
  journal = {Journal of Automated Reasoning},
  volume = 56,
  number = 4,
  pages = {387--457}
}
@article{bobot14sttt,
  topics = {team},
  doi = {10.1007/s10009-014-0314-5},
  hal_id = {hal-00967132},
  hal = {http://hal.inria.fr/hal-00967132/en},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
  title = {Let's Verify This with {Why3}},
  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
  volume = 17,
  number = 6,
  pages = {709--727},
  year = 2015,
  note = {See also \url{http://toccata.lri.fr/gallery/fm2012comp.en.html}},
  publisher = {Springer Berlin / Heidelberg},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {STTT},
  x-international-audience = {yes},
  x-editorial-board = {yes}
}
@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.
  }
}
@article{gondelman16fmsd,
  author = {Jean-Christophe Filli\^atre and L\'eon
            Gondelman and Andrei Paskevich},
  title = {The Spirit of Ghost Code},
  journal = {Formal Methods in System Design},
  publisher = {Springer},
  year = 2016,
  volume = 48,
  number = 3,
  pages = {152--174},
  issn = {1572-8102},
  doi = {10.1007/s10703-016-0243-x},
  topics = {team},
  hal = {https://hal.archives-ouvertes.fr/hal-01396864v1},
  keywords = {Why3},
  type_publi = {irevcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {revue},
  x-editorial-board = {yes},
  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 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{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},
  pages = {94--109},
  crossref = {vstte15},
  topics = {team,lri},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@techreport{gondelman16reg,
  topics = {team},
  author = {Jean-Christophe Filli\^atre and L\'eon
            Gondelman and Andrei Paskevich},
  title = {A Pragmatic Type System for Deductive Verification},
  type = {Research Report},
  institution = {Universit\'e Paris Sud},
  year = 2016,
  abstract = { In the context of deductive verication, it is customary
                  today to handle programs with pointers using either
                  separation logic, dynamic frames, or explicit memory
                  models. Yet we can observe that in numerous
                  programs, a large amount of code ts within the scope
                  of Hoare logic, provided we can statically control
                  aliasing. When this is the case, the code
                  correctness can be reduced to simpler verication
                  conditions which do not require any explicit memory
                  model. This makes verication conditions more
                  amenable both to automated theorem proving and to
                  manual inspection and debugging. In this paper, we
                  devise a method of such static aliasing control for
                  a programming language featuring nested data
                  structures with mutable components. Our solution is
                  based on a type system with singleton regions and
                  eects, which we prove to be sound.},
  hal = {https://hal.archives-ouvertes.fr/hal-01256434v3},
  note = {\url{https://hal.archives-ouvertes.fr/hal-01256434v3}}
}
@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{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{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{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{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},
  volume = 9593,
  publisher = {Springer}
}