Aleksey Veresov



Programming Languages, Formal Methods, Concurrent Programming

Current Affiliation

— Master's student in Computer Science, KTH 2022–present

My thesis will be about formal verification of epoch-based snapshotting, which is the algorithm used, for example, to ensure exactly-once processing in Apache Flink. My supervisors are Jonas Spenger and Philipp Haller.

— Software engineer, Hopsworks 2024–present

I don’t have much to say yet about this experience.

Appointments Held

— Research student assistant, KTH 2023–2024

I worked on Portals, a stateful dataflow system, mainly with Jonas Spenger and Philipp Haller. I was involved mostly in formalizing the system and a bit in programming it.

— Junior researcher, KIAM 2018–2022

I was involved in optimization of parallel programs and writing of scripts, and implemented elementary functions for FPGAs.

— Haskell backend programmer, MCCME 2021–2022

I worked on a website for learning school math. I implemented three web services backing it, and integrated support of authentication through a governmental system.


— B.Sc. in Applied Mathematics and Computer Science, Moscow State University 2016–2022

In my thesis, I describe a new method of embedding Lisp into C by providing a library which supports writing Lisp-like expressions directly as C expressions.

Other Activities

I helped with organisation of several mathematical conferences at Sirius, as well as attended two “summer” schools there: one on Complexity Theory and one on Formal Methods.

I wrote several programs and libraries in C (e.g. a little game inspired by the old Zelda games and a library for Common Gateway Interface).

Together with Nikita Orlov, we wrote a blog article on pitfalls of C with over a hundred thousands views (available only in Russian); made a little stack language compiling directly into machine code, and wrote a simple cipher encryptor and cracker in it; and finaly we designed and tinkered a M68k-based computer and wrote an emulator for it in Haskell.