Evgenii Kotelnikov, Ph.D.

I am a software developer and computer scientist specializing in static analysis, formal verification and functional programming. I hold a Ph.D. degree in computer science on the topic of formal methods. Over the past 10+ years I have worked as a software developer in all kinds of domains, from cloud security to self-driving cars. I have worked with many tech stacks over the years, right now my favourite ones are C, Python, Scala and Haskell.

Work experience

• Zenseact AB

  February 2021now

  Gothenburg, Sweden

  Software developer

  Zenseact develops an autonomous driving platform for Volvo Cars.

  • Develop safety critical software components of self-driving cars in C, C++ and Ada.
  • Scout for requirements, breakdown, refine and formalize.
  • Integrate the SPARK verification toolchain into the company's codebase.
  • Formally verify safety requirements of the core components in SPARK.
  • C
  • C++
  • Python
  • Ada
  • SPARK

• Ericsson AB

  August 2019January 2021

  Gothenburg, Sweden

  Software developer

  • Implemented new features for the control plane of SGSN-MME in Erlang.
  • Helped to migrate Ericsson's 5G platform from custom hardware to the telco cloud. Among other things, implemented a cloud-based storage and logging infrastructure for it.
  • Linux
  • Erlang
  • C
  • Bash
  • Python
  • Kubernetes
  • Docker

• Chalmers University of Technology

  September 2013September 2018

  Gothenburg, Sweden

  Doctoral researcher

  • Conducted research in the areas of automated theorem proving, formal methods and functional programming.
  • Published and presented academic results in conferences and workshops (see my Google Scholar profile).
  • Actively contributed to Vampire, a state-of-the-art automated theorem prover for first-order logic.
  • Assisted to preparing assignments, conducting consultation sessions and grading exams in the courses on Functional Programming, Databases, Algorithms and Datastructures.
  • Developed and maintained a homework submission system in the Computer Science department used annually by approx. 1000 students and 20 faculty members.
  • Java
  • Haskell
  • Python
  • PostgreSQL
  • Oracle Database

• Amazon Web Services

  March 2017June 2017

  New York, USA

  Applied scientist intern, Automated Reasoning Group

  Implemented an experimental backend for Tiros — a static analyzer of AWS virtual private cloud networks.

  • Scala
  • Python
  • Datalog
  • Vampire
  • Z3

• Yandex Inc.

  March 2011August 2013

  Saint Petersburg, Russia

  Software developer

  • Developed the back end of high-load web search services, including an in-house performant database solution capable of serving up to 400 requests per second.
  • Developed information retrieval tools and web crawlers.
  • Developed an app recommendation system for Yandex.Store.
  • Java
  • Scala
  • Akka
  • Oracle Database
  • MongoDB
  • Redis

• Motorola Solutions Inc.

  July 2010December 2010

  Saint Petersburg, Russia

  Software engineering intern

  Designed a specification language for low-level telecom protocols and implemented a toolchain for it.

  • Lisp
  • C
  • Python
  • Wireshark

• Freelance

  20052010

  Remote

  Web developer

  Developed front end and back end of commercial websites.

  • PHP
  • MySQL
  • HTML
  • CSS
  • JavaScript
  • jQuery

Education

• Doctor of philosophy (Ph.D.)

  September 2013September 2018

  Gothenburg, Sweden

  Chalmers University of Technology, Department of Computer Science and Engineering

  Thesis in computer science titled Automated Theorem Proving with Extensions of First-Order Logic

  Ph.D. supervisors Laura Kovács and Andrei Voronkov

  Explored ways to make automated theorem provers more efficient for applications by extending the logic that they reason in. The applications include automation of proof assistants and static analysis of software and networks.

  • Automated theorem proving
  • Formal methods
  • First-order logic
  • Static analysis
  • Vampire

• Master of science (M.Sc.)

  September 2011July 2013

  Saint Petersburg, Russia

  St Petersburg University, Department of Applied Mathematics

  Thesis in computer science titled Syntactical Extensions of Scala for Effectful Computations

  • Scala
  • Metaprogramming
  • Monads
  • Computational effects

• Bachelor of science (B.Sc.)

  September 2007July 2011

  Saint Petersburg, Russia

  St Petersburg University, Department of Applied Mathematics

  Thesis in computer science titled Source Code Generation Based on Language Grammar Description

  • Source code generation
  • Context-free grammars
  • Algebraic data types
  • Scheme

Public software projects

• vampireC++

  20142018

  An award-winning automated theorem prover for first-order logic.

• voogieHaskell

  2018

  A verification conditions generator for the Boogie intermediate verification language.

• scala-workflowScala

  2013

  An extension to Scala for boilerplate-free syntax for effectful computations.

• atomizerErlang

  2019

  A static analysis tool for finding loose atoms in large Erlang code bases.

• atpHaskell

  2019

  Haskell interface to automated theorem provers.

• firePythonHTMLCoffeeScriptDocker

  20142018

  A submission system for homework assignments.