Evgenii Kotelnikov
Ph.D. student in Computer Science department at Chalmers University of Technology
evgeny.kotelnikov@gmail.com, +46 31 772 17 57
- Postal address
- 412 96, Rännvägen 6, Gothenburg, Sweden
- Visiting address
- EDIT-building, room 5447
Ph.D. student in Computer Science department at Chalmers University of Technology
evgeny.kotelnikov@gmail.com, +46 31 772 17 57
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.
G. Sutcliffe and E. Kotelnikov. In Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning, pages 72–87, 2018.
An extension of the TPTP language that contains features of FOOL.
E. Kotelnikov, L. Kovács and A. Voronkov. In Proceedings of the 9th International Joint Conference on Automated Reasoning, pages 405–421, 2018.
A technique for efficient representation of imperative programs in FOOL.
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 doctor of philosophy (Ph.D.), Department of Computer Science and Engineering, Chalmers University of Technology, 2018.
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, PSI-2017, TACAS 2018, FM 2018 and iFM 2018.
I keep track of the cities I visited. I am on Twitter and Facebook. I do most of the hacking on GitHub.