default search action
Andrei Paskevich
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2021
- [e3]José Proença, Andrei Paskevich:
Proceedings of the 6th Workshop on Formal Integrated Development Environment, F-IDE@NFM 2021, Held online, 24-25th May 2021. EPTCS 338, 2021 [contents] - 2020
- [j6]Martin Clochard, Claude Marché
, Andrei Paskevich:
Deductive verification with ghost monitors. Proc. ACM Program. Lang. 4(POPL): 2:1-2:26 (2020) - [c20]Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, Andrei Paskevich:
Verification of Programs with Pointers in SPARK. ICFEM 2020: 55-72 - [c19]Jean-Christophe Filliâtre, Andrei Paskevich:
Abstraction and Genericity in Why3. ISoLA (1) 2020: 122-142
2010 – 2019
- 2018
- [i1]Georges-Axel Jaloyan, Yannick Moy, Andrei Paskevich:
Borrowing Safe Pointers from Rust in SPARK. CoRR abs/1805.05576 (2018) - 2017
- [e2]Andrei Paskevich, Thomas Wies:
Verified Software. Theories, Tools, and Experiments - 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers. Lecture Notes in Computer Science 10712, Springer 2017, ISBN 978-3-319-72307-5 [contents] - 2016
- [j5]Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich:
The spirit of ghost code. Formal Methods Syst. Des. 48(3): 152-174 (2016) - [j4]Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich:
Adding Decision Procedures to SMT Solvers Using Axioms with Triggers. J. Autom. Reason. 56(4): 387-457 (2016) - [c18]Alexander V. Lyaletski, Alexandre Lyaletsky, Andrei Paskevich:
Evidential Paradigm as Formal Knowledge Presentation and Processing. ICTERI 2016: 25-32 - 2015
- [j3]François Bobot
Let's verify this with Why3. Int. J. Softw. Tools Technol. Transf. 17(6): 709-727 (2015) - [c17]Martin Clochard, Jean-Christophe Filliâtre, Andrei Paskevich:
How to Avoid Proving the Absence of Integer Overflows. VSTTE 2015: 94-109 - [e1]Cezary Kaliszyk
Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015. EPTCS 186, 2015 [contents] - 2014
- [c16]Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich:
The Spirit of Ghost Code. CAV 2014: 1-16 - [c15]Martin Clochard, Claude Marché, Andrei Paskevich:
Verified programs with binders. PLPV 2014: 29-40 - [c14]Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich:
Formalizing Semantics with an Automatic Program Verifier. VSTTE 2014: 37-51 - 2013
- [c13]Jasmin Christian Blanchette, Andrei Paskevich:
TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. CADE 2013: 414-420 - [c12]Jean-Christophe Filliâtre, Andrei Paskevich:
Why3 - Where Programs Meet Provers. ESOP 2013: 125-128 - [c11]François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich:
Preserving User Proofs across Specification Changes. VSTTE 2013: 191-201 - 2012
- [c10]Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich:
Reasoning with Triggers. SMT@IJCAR 2012: 22-31 - [c9]Jean-Christophe Filliâtre, Andrei Paskevich, Aaron Stump:
The 2nd Verified Software Competition: Experience Report. COMPARE 2012: 36-49 - 2011
- [c8]François Bobot
Expressing Polymorphic Types in a Many-Sorted Language. FroCoS 2011: 87-102 - 2010
- [c7]Evelyne Contejean, Andrey Paskevich, Xavier Urbain, Pierre Courtieu, Olivier Pons, Julien Forest:
A3PAT, an approach for certified automated termination proofs. PEPM 2010: 63-72
2000 – 2009
- 2008
- [j2]Andrey Paskevich:
Connection Tableaux with Lazy Paramodulation. J. Autom. Reason. 40(2-3): 179-194 (2008) - [c6]Konstantin Verchinine, Alexander V. Lyaletski
On Correctness of Mathematical Texts from a Logical and Practical Point of View. AISC/MKM/Calculemus 2008: 583-598 - 2007
- [c5]Konstantin Verchinine, Alexander V. Lyaletski, Andrey Paskevich:
System for Automated Deduction (SAD): A Tool for Proof Verification. CADE 2007: 398-403 - 2006
- [j1]Alexander V. Lyaletski
SAD as a mathematical assistant - how should we go from here to there? J. Appl. Log. 4(4): 560-591 (2006) - [c4]Andrey Paskevich:
Connection Tableaux with Lazy Paramodulation. IJCAR 2006: 112-124 - 2004
- [c3]Alexander V. Lyaletski, Anatoly E. Doroshenko, Andrey Paskevich, Konstantin Verchinine:
Evidential Paradigm and Intelligent Mathematical Text Processing. ISTA 2004: 205-211 - [c2]Alexander V. Lyaletski
Theorem Proving and Proof Verification in the System SAD. MKM 2004: 236-250 - 2002
- [c1]Alexander V. Lyaletski, Konstantin Verchinine, Anatoli Degtyarev, Andrey Paskevich:
System for Automated Deduction (SAD): Linguistic and Deductive Peculiarities. Intelligent Information Systems 2002: 413-422
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-24 23:11 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: