Accéder directement au contenu
AP

Andrei Paskevich

11
Documents
Identifiants chercheurs

Présentation

Publications

claude-marche
Image document

Let's Verify This with Why3

François Bobot , Jean-Christophe Filliâtre , Claude Marché , Andrei Paskevich
International Journal on Software Tools for Technology Transfer, 2015, 17 (6), pp.709-727. ⟨10.1007/s10009-014-0314-5⟩
Article dans une revue hal-00967132v1
Image document

Des transformations logiques passent leur certificat

Quentin Garchery , Chantal Keller , Claude Marché , Andrei Paskevich
JFLA 2020 - Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France
Communication dans un congrès hal-02384946v2
Image document

Deductive Verification with Ghost Monitors

Martin Clochard , Claude Marché , Andrei Paskevich
POPL 2020 - 47th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2020, New Orleans, United States. ⟨10.1145/3371070⟩
Communication dans un congrès hal-02368284v1
Image document

Formalizing Semantics with an Automatic Program Verifier

Martin Clochard , Jean-Christophe Filliâtre , Claude Marché , Andrei Paskevich
6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria
Communication dans un congrès hal-01067197v1
Image document

Verified Programs with Binders

Martin Clochard , Claude Marché , Andrei Paskevich
Programming Languages meets Program Verification, Jan 2014, San Diego, United States
Communication dans un congrès hal-00913431v1
Image document

Preserving User Proofs Across Specification Changes

François Bobot , Jean-Christophe Filliâtre , Claude Marché , Guillaume Melquiond , Andrei Paskevich
Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. pp.191-201
Communication dans un congrès hal-00875395v1
Image document

Why3: Shepherd Your Herd of Provers

François Bobot , Jean-Christophe Filliâtre , Claude Marché , Andrei Paskevich
Boogie 2011: First International Workshop on Intermediate Verification Languages, 2011, Wroclaw, Poland. pp.53-64
Communication dans un congrès hal-00790310v1

Why3 version 1.0

Jean-Christophe Filliâtre , Andrei Paskevich , Guillaume Melquiond , Claude Marché , François Bobot
France, N° de brevet: IDDN.FR.001.420003.000.S.P.2019.000.20600. 2018
Brevet hal-03136256v1
Image document

Deductive Verification via Ghost Debugging

Martin Clochard , Andrei Paskevich , Claude Marché
[Research Report] RR-9219, Inria Saclay Ile de France. 2018
Rapport hal-01907894v1