paskevich.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc paskevich.cite -ob paskevich.bib -c 'author : "paskevich"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../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.org/}}
}
@misc{why3,
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},
topics = {team},
keywords = {Why3},
note = {\url{http://why3.org/}}
}
@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.org/download/manual-0.81.pdf},
note = {\url{http://why3.org/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.org/download/manual-0.82.pdf},
note = {\url{http://why3.org/download/manual-0.82.pdf}}
}
@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.org/download/manual-0.86.1.pdf},
note = {\url{http://why3.org/download/manual-0.86.1.pdf}}
}
@inproceedings{boogie11why3-short,
crossref = {boogie11why3},
booktitle = {Boogie},
address = {},
topics = {}
}
@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}
}
@inproceedings{BobotPaskevich2011frocos-short,
author = {Fran\c{c}ois Bobot and Andrei Paskevich},
title = {{Expressing Polymorphic Types in a Many-Sorted Language}},
booktitle = {FroCoS},
series = {LNCS},
volume = {6989},
year = {2011},
pages = {87--102}
}
@misc{vscomp2012,
author = {Jean-Christophe Filli\^atre and Andrei Paskevich and Aaron Stump},
title = {The 2nd {V}erified {S}oftware {C}ompetition},
month = {November},
year = 2011,
note = {\url{https://sites.google.com/site/vstte2012/compet}}
}
@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 = {https://usr.lmf.cnrs.fr/~jcf/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-short,
crossref = {filliatre13esop},
booktitle = {ESOP},
series = {LNCS},
editor = {},
topics = {}
}
@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.gitlabpages.inria.fr/toccata/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}}
}
@techreport{fgpps18,
author = {Jean-Christophe Filli{\^a}tre and L{\'e}on Gondelman and
Andrei Paskevich and M{\'a}rio Pereira and Sim{\~a}o Melo de Sousa},
title = {A Toolchain to {P}roduce {C}orrect-by-{C}onstruction {OC}aml
{P}rograms},
hal = {https://hal.inria.fr/hal-01783851},
pdf = {https://hal.inria.fr/hal-01783851/file/main.pdf},
note = {artifact: \url{https://www.lri.fr/~mpereira/correct_ocaml.ova}},
year = {2018}
}
@techreport{clochard18rr,
topics = {team},
title = {Deductive Verification via Ghost Debugging},
author = {Clochard, Martin and Paskevich, Andrei and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-01907894},
type = {Research Report},
number = 9219,
institution = {Inria},
year = 2018
}
@inproceedings{clochard20popl,
topics = {team},
title = {Deductive Verification with Ghost Monitors},
author = {Clochard, Martin and March\'e, Claude and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-02368284},
booktitle = {Principles of Programming Languages},
address = {New Orleans, United States},
year = 2020,
doi = {10.1145/3371070}
}
@unpublished{jaloyan18,
topics = {team},
title = {Verification of Programs with Pointers in {SPARK}},
author = {Jaloyan, Georges-Axel and Dross, Claire and Maalej, Maroua and Moy, Yannick and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-01936105},
note = {working paper \url{https://hal.inria.fr/hal-01936105}},
year = 2018,
month = nov
}
@techreport{huisman19rr,
topics = {team},
title = {VerifyThis 2018: A Program Verification Competition},
author = {Huisman, Marieke and Monahan, Rosemary and M{\"u}ller, Peter and Paskevich, Andrei and Ernst, Gidon},
hal = {https://hal.inria.fr/hal-01981937},
type = {Research Report},
institution = {Universit{\'e} Paris-Saclay},
year = 2019,
month = jan
}
@inproceedings{garchery20jfla,
topics = {team},
title = {Des transformations logiques passent leur certicat},
author = {Garchery, Quentin and Keller, Chantal and March{\'e}, Claude and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-02384946},
crossref = {jfla20}
}
@inproceedings{paskevich20isola,
author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
title = {Abstraction and Genericity in {Why3}},
booktitle = {9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)},
month = oct,
year = 2020,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 12476,
pages = {122--142},
editor = {Tiziana Margaria and Bernhard Steffen},
address = {Rhodes, Greece},
topics = {team},
note = {See also \url{https://usr.lmf.cnrs.fr/~jcf/isola-2020/}},
hal = {https://hal.inria.fr/hal-02696246}
}
@inproceedings{jaloyan20icfem,
topics = {team},
title = {Verification of Programs with Pointers in {SPARK}},
author = {Jaloyan, Georges-Axel and Dross, Claire and Maalej, Maroua and Moy, Yannick and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-03094566},
booktitle = {Formal Methods and Software Engineering (ICFEM)},
pages = {55--72},
year = 2020,
doi = {10.1007/978-3-030-63406-3\_4}
}
@misc{VerifyThis2021DLLtoBST,
title = {Solution to VerifyThis 2021 challenge 2},
author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
year = {2021},
note = {\url{https://toccata.gitlabpages.inria.fr/toccata/gallery/verifythis_2021_dll_to_bst.en.html}}
}
@inproceedings{filliatre23jfla,
topics = {team},
title = {L'arithm{\'e}tique de s{\'e}paration},
author = {Filli{\^a}tre, Jean-Christophe and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-03886759},
booktitle = {JFLA 2023 - 34{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs},
editor = {Timothy Bourke and Delphine Demange},
pages = {274--283},
year = 2023
}
@unpublished{paskevich:hal-04115885,
title = {{Flexible Verification Conditions with Continuations and Barriers}},
author = {Paskevich, Andrei},
url = {https://inria.hal.science/hal-04115885},
note = {\url{https://inria.hal.science/hal-04115885}},
year = {2023},
month = sep,
pdf = {https://inria.hal.science/hal-04115885v3/file/coma.pdf},
hal_id = {hal-04115885},
hal_version = {v3}
}
@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{jfla20,
title = {Trente-et-uni\`emes Journ\'ees Francophones des Langages Applicatifs},
booktitle = {Trente-et-uni\`emes Journ{\'e}es Francophones des Langages Applicatifs},
address = {Gruissan, France},
year = 2020,
month = jan,
editor = {Dargaye, Zaynah and R\'egis-Gianas, Yann}
}
@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}
}