Accéder directement au contenu
AP

Andrei Paskevich

15
Documents
Identifiants chercheurs

Présentation

Publications

jean-christophe-filliatre
Image document

The Spirit of Ghost Code

Jean-Christophe Filliâtre , Léon Gondelman , Andrei Paskevich
Formal Methods in System Design, 2016, 48 (3), pp.152-174. ⟨10.1007/s10703-016-0243-x⟩
Article dans une revue hal-01396864v1
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

L'arithmétique de séparation

Jean-Christophe Filliâtre , Andrei Paskevich
JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.274-283
Communication dans un congrès hal-03886759v2
Image document

Abstraction and Genericity in Why3

Jean-Christophe Filliâtre , Andrei Paskevich
ISoLA 2021 - 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2021, Rhodes, Greece. ⟨10.1007/978-3-030-61362-4_7⟩
Communication dans un congrès hal-02696246v2
Image document

How to avoid proving the absence of integer overflows

Martin Clochard , Jean-Christophe Filliâtre , Andrei Paskevich
7th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2015, San Francisco, CA, United States
Communication dans un congrès hal-01162661v2
Image document

The Spirit of Ghost Code

Jean-Christophe Filliâtre , Léon Gondelman , Andrei Paskevich
CAV 2014, Computer Aided Verification - 26th International Conference, Jul 2014, Vienna Summer Logic 2014, Austria
Communication dans un congrès hal-00873187v3
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

Why3 -- Where Programs Meet Provers

Jean-Christophe Filliâtre , Andrei Paskevich
ESOP'13 22nd European Symposium on Programming, Mar 2013, Rome, Italy
Communication dans un congrès hal-00789533v1
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

The 2nd Verified Software Competition: Experience Report

Jean-Christophe Filliâtre , Andrei Paskevich , Aaron Stump
COMPARE 2012, Comparative Empirical Evaluation of Reasoning Systems, 1st Intl. Workshop, Jun 2012, Manchester, United Kingdom. pp.36-49
Communication dans un congrès hal-00798777v1
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