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