- 29
- 1
- 1
- 1
AP
Andrei Paskevich
32
Documents
Identifiants chercheurs
tertium- IdRef : 204772567
Présentation
Publications
- 4
- 3
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 15
- 11
- 5
- 4
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 2
- 1
- 1
- 4
- 1
- 4
- 3
- 2
- 3
- 5
- 2
- 2
- 1
- 1
- 3
- 2
- 1
- 1
|
|
Adding Decision Procedures to SMT Solvers using Axioms with TriggersJournal of Automated Reasoning, 2016, 56 (4), pp.387-457. ⟨10.1007/s10817-015-9352-2⟩
Article dans une revue
hal-01221066v1
|
|
|
The Spirit of Ghost CodeFormal Methods in System Design, 2016, 48 (3), pp.152-174. ⟨10.1007/s10703-016-0243-x⟩
Article dans une revue
hal-01396864v1
|
|
|
Let's Verify This with Why3International 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
|
|
|
L'arithmétique de séparationJFLA 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
|
|
|
Abstraction and Genericity in Why3ISoLA 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
|
|
|
Deductive Verification with Ghost MonitorsPOPL 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
|
|
|
Verification of Programs with Pointers in SPARKICFEM 2020 - 22nd International Conference on Formal Engineering Methods, Mar 2020, Singapore / Virtual, Singapore. pp.55-72, ⟨10.1007/978-3-030-63406-3_4⟩
Communication dans un congrès
hal-03094566v1
|
|
|
Des transformations logiques passent leur certificatJFLA 2020 - Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France
Communication dans un congrès
hal-02384946v2
|
|
|
How to avoid proving the absence of integer overflows7th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2015, San Francisco, CA, United States
Communication dans un congrès
hal-01162661v2
|
|
|
The Spirit of Ghost CodeCAV 2014, Computer Aided Verification - 26th International Conference, Jul 2014, Vienna Summer Logic 2014, Austria
Communication dans un congrès
hal-00873187v3
|
|
|
Verified Programs with BindersProgramming Languages meets Program Verification, Jan 2014, San Diego, United States
Communication dans un congrès
hal-00913431v1
|
|
|
Formalizing Semantics with an Automatic Program Verifier6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria
Communication dans un congrès
hal-01067197v1
|
|
|
Preserving User Proofs Across Specification ChangesFifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. pp.191-201
Communication dans un congrès
hal-00875395v1
|
|
|
TFF1: The TPTP Typed First-Order Form with Rank-1 PolymorphismCADE - 24th International Conference on Automated Deduction - 2013, Jun 2013, Lake Placid, NY, United States. pp.414-420
Communication dans un congrès
hal-00825086v1
|
|
|
Why3 -- Where Programs Meet ProversESOP'13 22nd European Symposium on Programming, Mar 2013, Rome, Italy
Communication dans un congrès
hal-00789533v1
|
|
|
The 2nd Verified Software Competition: Experience ReportCOMPARE 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
|
|
|
Why3: Shepherd Your Herd of ProversBoogie 2011: First International Workshop on Intermediate Verification Languages, 2011, Wroclaw, Poland. pp.53-64
Communication dans un congrès
hal-00790310v1
|
|
|
A3PAT, an Approach for Certified Automated Termination Proofs2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, ACM, Jan 2010, Madrid, Spain. pp.63-72, ⟨10.1145/1706356.1706370⟩
Communication dans un congrès
inria-00535655v1
|
Why3 version 1.0France, N° de brevet: IDDN.FR.001.420003.000.S.P.2019.000.20600. 2018
Brevet
hal-03136256v1
|
|
|
The Why3 platform 0.812013
Autre publication scientifique
hal-00822856v1
|
|
|
Flexible Verification Conditions with Continuations and Barriers2023
Pré-publication, Document de travail
hal-04115885v3
|
|
|
Continuation Passing as an Abstract Syntax for Deductive Verification2022
Pré-publication, Document de travail
hal-03115120v2
|
|
|
A Toolchain to Produce Verified OCaml Libraries2020
Pré-publication, Document de travail
hal-01783851v2
|
|
|
Deductive Verification with Ghost Monitors2018
Pré-publication, Document de travail
hal-01926659v1
|
|
|
Verification of Programs with Pointers in SPARK2018
Pré-publication, Document de travail
hal-01936105v1
|
|
|
A Pragmatic Type System for Deductive Verification2016
Pré-publication, Document de travail
hal-01256434v3
|
|
|
Adding Decision Procedures to SMT Solvers using Axioms with Triggers2013
Pré-publication, Document de travail
hal-00915931v1
|
|
|
VerifyThis 2018: A Program Verification Competition[Research Report] Université Paris-Saclay. 2019
Rapport
hal-01981937v1
|
|
|
Deductive Verification via Ghost Debugging[Research Report] RR-9219, Inria Saclay Ile de France. 2018
Rapport
hal-01907894v1
|
|
|
Reasoning with Triggers[Research Report] RR-7986, INRIA. 2012, pp.29
Rapport
hal-00703207v1
|
|
|
Expressing Polymorphic Types in a Many-Sorted Language[Research Report] 2011
Rapport
inria-00591414v4
|
|
|
Algebraic types and pattern matching in the logical language of the Why verification platform[Research Report] RR-7128, INRIA. 2009
Rapport
inria-00439232v2
|