Relational interpreters are traditional research subjects in relational programming due to a number of reasons. First, an interpreter for a Turing-complete language is a non-trivial and at the same time observable program to be used as a testbench for relational language implementation. Second, relational interpreter makes it possible to evaluate regular programs in relational semantics. Finally, due to a “multidirectional’’ nature of relational interpreters certain program synthesis problems can be solved. However, state-of-the art relational language implementations do not allow to express synthesis problems in a conventional form “programs from specifications”.

We describe a slightly different approach to program synthesis based on the idea of turning verifiers into solvers via program inversion. This (not quite a new) approach has a number of advantages. First, it allows to specify more program synthesis problems while still sticking with existing relational implementations. Second, it to some extent cures an inherent to program synthesis “debugging of specifications instead of debugging of implementations’’ illness. As an additional step we use relational conversion (a transformation of functional programs into relational ones) which makes it possible to eliminate the need for tedious relational encoding of verifiers.

• 1989-1994 — master program at Saint Petersburg State University, Faculty of Mathematics and Mechanics, computer science department.
• 1999 - present time — Saint Petersburg State University, Faculty of Mathematics and Mechanics, chair of Software Engineering.
• 2004 - PhD in Computer Science.
• 2012 - 2022 — JetBrains Research, Programming Languages and Tools Laboratory supervisor.