I was born in 1979 in Kiev (Soviet Union at the time, Ukraine now). These days, I live in Orsay, France. I am maître de conférences (associate professor) at Paris-Sud 11 University, IUT d'Orsay. My research affiliation is Laboratoire de Recherche en Informatique (LRI), team ProVal. You can find here my curriculum vitæ (eng, fra) and my publications.
I do research in automated reasoning. My doctorate thesis «Methods of formalization of mathematical knowledge and reasoning» was prepared under the joint supervision of Konstantin Verchinine at Paris 12 University and Alexander Lyaletski and Vladimir Donchenko at Kiev National University. I received the diploma of Candidate of physical and mathematical sciences from KNU in 2005 and the diploma of Doctor of informatics with high honors from Paris 12 in 2007. I participated in several international and local scientific projects supported by INTAS, Egide-Dnipro, and ANR. Before taking a position at IUT d'Orsay, I taught for three years at IUT Sénart/Fontainebleau.
My research activity so far was mainly connected to the Evidence Algorithm project. We develop a mathematical assistant, called System for Automated Deduction (SAD) and intended for automated verification of formal mathematical texts. SAD processes texts written in ForTheL, a kind of controlled English language that closely follows the natural language and style of mathematical publications. The SAD system is implemented in Haskell and distributed under GNU GPL. You can also enjoy it through a web interface.
During the last year, I participated in the development of
a tool for certification of termination proofs for
term rewriting systems and also an automated termination prover.
Recently, I started working on a software verification tool