← Publications
-
[1]
-
Dross, C., Conchon, S., Kanig, J., and Paskevich, A.
Adding decision procedures to SMT solvers using axioms with
triggers.
Journal of Automated Reasoning 56, 4 (2016), 387--457.
[ bib |
.pdf |
Abstract ]
-
[2]
-
Clochard, M., Filliâtre, J.-C., and Paskevich, A.
How to avoid proving the absence of integer overflows.
In VSTTE 2015, 7th Working Conference on Verified Software:
Theories, Tools and Experiments (July 2015), A. Gurfinkel and S. A.
Seshia, Eds.
[ bib |
.pdf |
Abstract ]
-
[3]
-
Filliâtre, J.-C., Gondelman, L., and Paskevich, A.
The spirit of ghost code.
In CAV 2014, 26th International Conference on Computer Aided
Verification (July 2014), A. Biere and R. Bloem, Eds., vol. 8559 of
Lecture Notes in Computer Science, Springer, pp. 1--16.
[ bib |
.pdf |
Abstract ]
-
[4]
-
Clochard, M., Filliâtre, J.-C., Marché, C., and Paskevich, A.
Formalizing semantics with an automatic program verifier.
In VSTTE 2014, 6th International Conference on Verified
Software: Theories, Tools, Experiments (July 2014), D. Giannakopoulou and
D. Kroening, Eds., Lecture Notes in Computer Science, Springer.
[ bib |
.pdf |
Abstract ]
-
[5]
-
Clochard, M., Marché, C., and Paskevich, A.
Verified programs with binders.
In PLPV 2014, ACM SIGPLAN Workshop on Programming Languages
meets Program Verification (2014), ACM Press, pp. 29--40.
[ bib |
.pdf |
Abstract ]
-
[6]
-
Bobot, F., Filliâtre, J.-C., Marché, C., and Paskevich, A.
Let's verify this with Why3.
International Journal on Software Tools for Technology
Transfer (2014).
[ bib |
http |
.pdf |
Abstract ]
-
[7]
-
Blanchette, J. C., and Paskevich, A.
TFF1: The TPTP typed first-order form with rank-1 polymorphism.
In CADE 2013, 24th International Conference on Automated
Deduction (June 2013), M. P. Bonacina, Ed., vol. 7898 of Lecture
Notes in Computer Science, Springer, pp. 414--420.
[ bib |
.pdf |
Abstract ]
-
[8]
-
Bobot, F., Filliâtre, J.-C., Marché, C., Melquiond, G., and Paskevich,
A.
Preserving user proofs across specification changes.
In VSTTE 2013, 5th International Conference on Verified
Software: Theories, Tools, Experiments (May 2013), E. Cohen and
A. Rybalchenko, Eds., vol. 8164 of Lecture Notes in Computer Science,
Springer, pp. 191--201.
[ bib |
.pdf |
Abstract ]
-
[9]
-
Filliâtre, J.-C., and Paskevich, A.
Why3 --- where programs meet provers.
In ESOP 2013, Proceedings of the 22nd European Symposium on
Programming (Mar. 2013), M. Felleisen and P. Gardner, Eds., vol. 7792 of
Lecture Notes in Computer Science, Springer, pp. 125--128.
[ bib |
.pdf |
Abstract ]
-
[10]
-
Dross, C., Conchon, S., Kanig, J., and Paskevich, A.
Reasoning with triggers.
In SMT 2012, 10th International Workshop on Satisability Modulo
Theories (Manchester, UK, June 2012), P. Fontaine and A. Goel, Eds.,
pp. 22--31.
[ bib |
.pdf |
Abstract ]
-
[11]
-
Dross, C., Conchon, S., Kanig, J., and Paskevich, A.
Reasoning with triggers.
Research Report RR-7986, INRIA, June 2012.
[ bib |
http |
.pdf |
Abstract ]
-
[12]
-
Filliâtre, J.-C., Paskevich, A., and Stump, A.
The 2nd verified software competition: Experience report.
In COMPARE2012, 1st International Workshop on Comparative
Empirical Evaluation of Reasoning Systems (Manchester, UK, June 2012),
V. Klebanov, B. Beckert, A. Biere, and G. Sutcliffe, Eds., vol. 873 of
CEUR Workshop Proceedings, pp. 36--49.
[ bib |
.pdf |
Abstract ]
-
[13]
-
Bobot, F., and Paskevich, A.
Expressing polymorphic types in a many-sorted language.
In FroCoS 2011, 8th International Symposium on Frontiers of
Combining Systems (Saarbrücken, Germany, Oct. 2011), C. Tinelli and
V. Sofronie-Stokkermans, Eds., vol. 6989 of Lecture Notes in Computer
Science, Springer, pp. 87--102.
[ bib |
.pdf |
Abstract ]
-
[14]
-
Bobot, F., and Paskevich, A.
Expressing polymorphic types in a many-sorted language, July 2011.
Extended report.
[ bib |
http |
.pdf |
Abstract ]
-
[15]
-
Bobot, F., Filliâtre, J.-C., Marché, C., and Paskevich, A.
Why3: Shepherd your herd of provers.
In Boogie 2011, First International Workshop on Intermediate
Verification Languages (Wrocław, Poland, Aug. 2011), pp. 53--64.
[ bib |
.pdf |
Abstract ]
-
[16]
-
Contejean, É., Courtieu, P., Forest, J., Paskevich, A., Pons, O., and
Urbain, X.
A3PAT, an approach for certified automated termination proofs.
In PEPM'10, Proceedings of the 2010 ACM SIGPLAN Workshop on
Partial Evaluation and Program Manipulation (Madrid, Spain, Jan. 2010),
ACM, pp. 63--72.
[ bib |
DOI |
.pdf |
Abstract ]
-
[17]
-
Verchinine, K., Lyaletski, A., Paskevich, A., and Anisimov, A.
On correctness of mathematical texts from a logical and practical
point of view.
In Intelligent Computer Mathematics, AISC/Calculemus/MKM 2008
(Birmingham, United Kingdom, July 2008), S. Autexier, J. Campbell, J. Rubio,
V. Sorge, M. Suzuki, and F. Wiedijk, Eds., vol. 5144 of Lecture Notes in
Computer Science, Springer, pp. 583--598.
[ bib |
.pdf |
Abstract ]
-
[18]
-
Paskevich, A.
Connection tableaux with lazy paramodulation.
Journal of Automated Reasoning 40, 2--3 (2008), 179--194.
[ bib |
.pdf |
Abstract ]
-
[19]
-
Paskevych, A.
Méthodes de formalisation des connaissances et des
raisonnements mathématiques: aspects appliqués et théoriques.
PhD thesis, Université Paris 12, 2007.
In French.
[ bib |
.pdf |
Abstract ]
-
[20]
-
Paskevich, A., Verchinine, K., Lyaletski, A., and Anisimov, A.
Reasoning inside a formula and ontological correctness of a formal
mathematical text.
In Calculemus/MKM 2007 --- Work in Progress (Hagenberg,
Austria, June 2007), M. Kauers, M. Kerber, R. Miner, and W. Windsteiger,
Eds., no. 07-06 in RISC-Linz Report Series, University of Linz, Austria,
pp. 77--91.
[ bib |
.pdf |
Abstract ]
-
[21]
-
Verchinine, K., Lyaletski, A., and Paskevich, A.
System for Automated Deduction (SAD): a tool for proof
verification.
In Automated Deduction, 21st International Conference,
CADE-21 (Bremen, Germany, July 2007), F. Pfenning, Ed., vol. 4603 of
Lecture Notes in Computer Science, Springer, pp. 398--403.
[ bib |
.pdf |
Abstract ]
-
[22]
-
Paskevich, A.
Connection tableaux with lazy paramodulation.
In Automated Reasoning, 3rd International Joint Conference,
IJCAR 2006 (Seattle WA, USA, Aug. 2006), U. Furbach and N. Shankar, Eds.,
vol. 4130 of Lecture Notes in Computer Science, Springer, pp. 112--124.
[ bib |
.pdf |
Abstract ]
-
[23]
-
Lyaletski, A., Paskevich, A., and Verchinine, K.
SAD as a mathematical assistant --- how should we go from here to
there?
Journal of Applied Logic 4, 4 (2006), 560--591.
[ bib |
.ps.gz |
Abstract ]
-
[24]
-
Paskevych, A.
Methods of formalization of mathematical knowledge and
reasoning: theoretical and practical aspects.
PhD thesis, Kiev National Taras Shevchenko University, 2005.
In Ukrainian.
[ bib |
.pdf ]
-
[25]
-
Lyaletski, A., Verchinine, K., and Paskevich, A.
Theorem proving and proof verification in the system SAD.
In Mathematical Knowledge Management, 3rd International
Conference, MKM 2004 (Bialowieza, Poland, Sept. 2004), A. Asperti,
G. Bancerek, and A. Trybulec, Eds., vol. 3119 of Lecture Notes in
Computer Science, Springer, pp. 236--250.
[ bib |
.ps.gz |
Abstract ]
-
[26]
-
Lyaletski, A. V., Doroshenko, A. E., Paskevich, A., and Verchinine, K.
Evidential paradigm and intelligent mathematical text processing.
In Information Systems Technology and its Applications, 3rd
International Conference, ISTA 2004 (Salt Lake City UT, USA, July 2004),
A. E. Doroshenko, T. A. Halpin, S. W. Liddle, and H. C. Mayr, Eds., vol. 48
of Lecture Notes in Informatics, GI, pp. 205--211.
[ bib |
.pdf |
Abstract ]
-
[27]
-
Lyaletski, A., Verchinine, K., and Paskevich, A.
On verification tools implemented in the System for Automated
Deduction.
In Implementation Technology for Computational Logic Systems,
2nd CoLogNet Workshop, ITCLS 2003 (Pisa, Italy, Sept. 2003), pp. 3--14.
[ bib |
.ps.gz |
Abstract ]
-
[28]
-
Aselderov, Z., Verchinine, K., Degtyarev, A., Lyaletski, A., Paskevich,
A., and Pavlov, A.
Linguistic tools and deductive technique of the System for
Automated Deduction.
In Implementation of Logics, 3rd International Workshop, WIL
2002 (Tbilisi, Georgia, Oct. 2002), pp. 21--24.
[ bib |
.ps.gz |
Abstract ]
-
[29]
-
Lyaletski, A., Verchinine, K., Degtyarev, A., and Paskevich, A.
System for Automated Deduction (SAD): Linguistic and
deductive peculiarities.
In Intelligent Information Systems, 11th International
Symposium, IIS 2002 (Sopot, Poland, June 2002), M. A. Klopotek, S. T.
Wierzchon, and M. Michalewicz, Eds., Advances in Soft Computing,
Physica-Verlag, pp. 413--422.
[ bib |
.ps.gz |
Abstract ]
-
[30]
-
Lyaletski, A., and Paskevich, A.
Goal-driven inference search in classical propositional logic.
In Proc. International Workshop STRATEGIES'2001 (Siena,
Italy, June 2001), pp. 65--74.
[ bib |
.ps.gz |
Abstract ]
-
[31]
-
Vershinin, K., and Paskevich, A.
ForTheL --- the language of formal theories.
International Journal of Information Theories and Applications
7, 3 (2000), 120--126.
[ bib |
.ps.gz |
Abstract ]
to main page
Last update: 5 Sep 2015