I am interested in program analysis, automated theorem proving and functional programming. These days I am working on new features of the Vampire theorem prover that make it more attractive to deductive program verification. This is done as part of the TheProSE project. In my master's thesis I explored effectful computations in Scala.
My main academic advisor is Laura Kovács, and my co-advisors are Andrei Voronkov and Moa Johansson.
In the spring of 2017 I spent three months at AWS Security Automated Reasoning Group, led by Byron Cook, working on static analysis of networks using Vampire.
E. Kotelnikov, L. Kovács, M. Suda and A. Voronkov. In Proceedings of the 2nd Global Conference on Artificial Intelligence, pages 53–71, 2016.
A clausification algorithm for FOOL whose resuls are friendly for superposition-based reasoning.
E. Kotelnikov, L. Kovács, G. Reger and A. Voronkov. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pages 37–48, 2016.
An implementation of first class boolean sort and a polymorphic theory of arrays in Vampire.
E. Kotelnikov, L. Kovács and A. Voronkov. In Intelligent Computer Mathematics, pages 71–86, 2015.
A formalisation of first-order logic with a first class boolean sort, intended for superposition-based reasoning.
E. Kotelnikov. In Proceedings of the Fifth Annual Scala Workshop, pages 35–43, 2014.
Effectful computations with (applicative) functors and monads can be expressed in a direct style in Scala using untyped macros.
E. Kotelnikov. In Proceedings of the 2012 Joint International Conference on Human-Centered Computer Environments, pages 87–92, 2012.
Context-free grammars can be converted to definitions of algebraic data types and a grammar-safe pretty-printer.
Thesis for the degree of licentiate of engineering, Department of Computer Science and Engineering, Chalmers University of Technology, 2016.
Thesis for the degree of master of science, Faculty of Applied Mathematics and Control Processes, Saint-Petersburg State University, 2013.
I was a teaching assistant in the following courses at Chalmers:
I develop and maintain Fire, a lab submission system used in our department.
I was involved in reviewing for SCSS 2014, FM 2015, LPAR-20, CPP 2016, CICM 2016, FM 2016 and PSI-2017.
I was a student volunteer at ICFP 2014 and CADE-26.
I keep track of the cities I visited. I am on Twitter and Facebook. I do most of the hacking on GitHub.