Researcher in formal methods at ITMO University, specializing in SAT/SMT solving, symbolic execution, and program analysis. I develop educational materials and teach discrete mathematics, focusing on practical applications of formal verification in software engineering.

• kotlin-satlib — SAT solvers library for JVM
• sat-nexus — SAT solvers library for Rust
• discrete-math-course — Supplementary materials for Discrete Mathematics
• formal-methods-course — Educational resources for Formal Methods
• USVM — Symbolic execution engine for automated program analysis (core contributor)
• JacoDB — Java bytecode analysis framework with interprocedural analysis (core contributor)