Andrei Paskevich

22 papers A* 1A 2B 1C 1Misc 1Journal 5Unranked 8
YearRankTypeTitle / Venue / Authors
2025 B conf
When Separation Arithmetic is Enough.
iFM
Jean-Christophe Filliâtre, Andrei Paskevich, Olivier Danvy
2025 — conf
coma, an Intermediate Verification Language with Explicit Abstraction Barriers.
ESOP (2)
Andrei Paskevich, Paul Patault, Jean-Christophe Filliâtre
2021 — ed.
Proceedings of the 6th Workshop on Formal Integrated Development Environment, F-IDE@NFM 2021, Held online, 24-25th May 2021.
F-IDE@NFM
José Proença, Andrei Paskevich
2020 — conf
Abstraction and Genericity in Why3.
ISoLA (1)
Jean-Christophe Filliâtre, Andrei Paskevich
2020 J jnl
Deductive verification with ghost monitors.
Proc. ACM Program. Lang.
Martin Clochard, Claude Marché, Andrei Paskevich
2020 C conf
Verification of Programs with Pointers in SPARK.
ICFEM
Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, Andrei Paskevich
2018 J jnl
Borrowing Safe Pointers from Rust in SPARK.
CoRR
Georges-Axel Jaloyan, Yannick Moy, Andrei Paskevich
2017 — ed.
Verified Software. Theories, Tools, and Experiments - 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers
VSTTE
Andrei Paskevich, Thomas Wies
2016 J jnl
Adding Decision Procedures to SMT Solvers Using Axioms with Triggers.
J. Autom. Reason.
Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich
2016 Misc conf
Evidential Paradigm as Formal Knowledge Presentation and Processing.
ICTERI
Alexander V. Lyaletski, Alexandre Lyaletsky, Andrei Paskevich
2016 J jnl
The spirit of ghost code.
Formal Methods Syst. Des.
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich
2015 — conf
How to Avoid Proving the Absence of Integer Overflows.
VSTTE
Martin Clochard, Jean-Christophe Filliâtre, Andrei Paskevich
2015 J jnl
Let's verify this with Why3.
Int. J. Softw. Tools Technol. Transf.
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
2015 — ed.
Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015.
PxTP@CADE
Cezary Kaliszyk, Andrei Paskevich
2014 — conf
Formalizing Semantics with an Automatic Program Verifier.
VSTTE
Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
2014 A* conf
The Spirit of Ghost Code.
CAV
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich
2014 — conf
Verified programs with binders.
PLPV
Martin Clochard, Claude Marché, Andrei Paskevich
2013 — conf
Preserving User Proofs across Specification Changes.
VSTTE
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
2013 A conf
TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism.
CADE
Jasmin Christian Blanchette, Andrei Paskevich
2013 A conf
Why3 - Where Programs Meet Provers.
ESOP
Jean-Christophe Filliâtre, Andrei Paskevich
2012 — conf
Reasoning with Triggers.
SMT@IJCAR
Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich
2012 — conf
The 2nd Verified Software Competition: Experience Report.
COMPARE
Jean-Christophe Filliâtre, Andrei Paskevich, Aaron Stump