System for Automated Deduction (SAD): Linguistic and Deductive Peculiarities. - Alexander V. Lyaletski; Konstantin Verchinine; Anatoli Degtyarev; Andrey Paskevich (Intelligent Information Systems, 2002)

Evidential Paradigm and Intelligent Mathematical Text Processing. - Alexander V. Lyaletski; Anatoly E. Doroshenko; Andrey Paskevich; Konstantin Verchinine (ISTA, 2004)

Theorem Proving and Proof Verification in the System SAD. - Alexander V. Lyaletski; Andrey Paskevich; Konstantin Verchinine (MKM, 2004)

SAD as a mathematical assistant - how should we go from here to there? - Alexander V. Lyaletski; Andrey Paskevich; Konstantin Verchinine (J. Appl. Log., 2006)

System for Automated Deduction (SAD): A Tool for Proof Verification. - Konstantin Verchinine; Alexander V. Lyaletski; Andrey Paskevich (CADE, 2007)

On Correctness of Mathematical Texts from a Logical and Practical Point of View. - Konstantin Verchinine; Alexander V. Lyaletski; Andrey Paskevich; Anatoly V. Anisimov (AISC/MKM/Calculemus, 2008)

Connection Tableaux with Lazy Paramodulation. - Andrey Paskevich (J. Autom. Reason., 2008)

A3PAT, an approach for certified automated termination proofs. - Evelyne Contejean; Andrey Paskevich; Xavier Urbain; Pierre Courtieu; Olivier Pons; Julien Forest (PEPM, 2010)

Expressing Polymorphic Types in a Many-Sorted Language. - François Bobot; Andrey Paskevich (FroCoS, 2011)

Reasoning with Triggers. - Claire Dross; Sylvain Conchon; Johannes Kanig; Andrei Paskevich (SMT@IJCAR, 2012)

The 2nd Verified Software Competition: Experience Report. - Jean-Christophe Filliâtre; Andrei Paskevich; Aaron Stump (COMPARE, 2012)

TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. - Jasmin Christian Blanchette; Andrei Paskevich (CADE, 2013)

Why3 - Where Programs Meet Provers. - Jean-Christophe Filliâtre; Andrei Paskevich (ESOP, 2013)

Preserving User Proofs across Specification Changes. - François Bobot; Jean-Christophe Filliâtre; Claude Marché; Guillaume Melquiond; Andrei Paskevich (VSTTE, 2013)

Verified programs with binders. - Martin Clochard; Claude Marché; Andrei Paskevich (PLPV, 2014)

Formalizing Semantics with an Automatic Program Verifier. - Martin Clochard; Jean-Christophe Filliâtre; Claude Marché; Andrei Paskevich (VSTTE, 2014)

How to Avoid Proving the Absence of Integer Overflows. - Martin Clochard; Jean-Christophe Filliâtre; Andrei Paskevich (VSTTE, 2015)

Let's verify this with Why3. - François Bobot; Jean-Christophe Filliâtre; Claude Marché; Andrei Paskevich (Int. J. Softw. Tools Technol. Transf., 2015)

Evidential Paradigm as Formal Knowledge Presentation and Processing. - Alexander V. Lyaletski; Alexandre Lyaletsky; Andrei Paskevich (ICTERI, 2016)

The spirit of ghost code. - Jean-Christophe Filliâtre; Léon Gondelman; Andrei Paskevich (Formal Methods Syst. Des., 2016)

Adding Decision Procedures to SMT Solvers Using Axioms with Triggers. - Claire Dross; Sylvain Conchon; Johannes Kanig; Andrei Paskevich (J. Autom. Reason., 2016)

Borrowing Safe Pointers from Rust in SPARK. - Georges-Axel Jaloyan; Yannick Moy; Andrei Paskevich (CoRR, 2018)

Verification of Programs with Pointers in SPARK. - Georges-Axel Jaloyan; Claire Dross; Maroua Maalej; Yannick Moy; Andrei Paskevich (ICFEM, 2020)

Abstraction and Genericity in Why3. - Jean-Christophe Filliâtre; Andrei Paskevich (ISoLA (1), 2020)

Deductive verification with ghost monitors. - Martin Clochard; Claude Marché; Andrei Paskevich (Proc. ACM Program. Lang., 2020)

coma, an Intermediate Verification Language with Explicit Abstraction Barriers. - Andrei Paskevich; Paul Patault; Jean-Christophe Filliâtre (ESOP (2), 2025)