Dmitry Mordvinov

Dmitry Mordvinov

Research Groups


Dmitry graduated from Saint-Petersburg State University, Department of Software Engineering in 2013. He was participating in numerous R&D projects. After the internship in the University of Washington in 2016 he is mainly working on approaches for compositional unbounded verification (in application for .NET framework).

Professional Activity

  • Formal verification (symbolic execution, constrained Horn clauses solving, inductive invariants)
  • Program synthesis
  • Programming languages
  • Type systems
  • Robotics
  • Visual Programming


Beyond the elementary representations of program invariants over algebraic data type


Kostyukov Yurii, Dmitry Mordvinov, and Grigory Fedyukovich

Property Directed Inference of Relational Invariants

October 2019

D. Mordvinov, G. Fedyukovich

Proceedings of 19th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2019

Read more

On Satisfiability of Nominal Type Systems With Variance

July 2019

A. Misonizhnik, D. Mordvinov

33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Read more

SMT-based analysis of constraints on .NET types


Aleksandr Misonizhnik and Dmitry Mordvinov

CEUR: 44-52

TRIK studio: Technical introduction


Mordvinov Dmitry, Yurii Litvinov, and Timofey Bryksin

Open Innovations Association (FRUCT), 2017 20th Conference of. IEEE

Verifying Safety of Functional Programs with Rosette/Unbound


Dmitry Mordvinov and Grigory Fedyukovich

Synchronizing constrained horn clauses


Mordvinov, Dmitry, and Grigory Fedyukovich

LPAR, EPiC Series in Computing. EasyChair

Survey on formal methods in robotics


D. A. Mordvinov, Yu. V. Litvinov

SPbSPU Journal. Computer Science. Telecommunication and Control Systems, no. 1(236), 84–107