Dmitry Mordvinov


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


  • D. Mordvinov, G. Fedyukovich
    Proceedings of 19th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2019, October 2019
  • A. Misonizhnik, D. Mordvinov
    33rd European Conference on Object-Oriented Programming (ECOOP 2019), July 2019
  • Aleksandr Misonizhnik and Dmitry Mordvinov
    SMT-based analysis of constraints on .NET types
    CEUR: 44-52, 2018
  • Mordvinov Dmitry, Yurii Litvinov, and Timofey Bryksin
    TRIK studio: Technical introduction
    Open Innovations Association (FRUCT), 2017 20th Conference of. IEEE, 2017
  • Dmitry Mordvinov and Grigory Fedyukovich
    Verifying Safety of Functional Programs with Rosette/Unbound
  • Mordvinov, Dmitry, and Grigory Fedyukovich
    Synchronizing constrained horn clauses
    LPAR, EPiC Series in Computing. EasyChair, 2017
  • D. A. Mordvinov, Yu. V. Litvinov
    Survey on formal methods in robotics
    SPbSPU Journal. Computer Science. Telecommunication and Control Systems, no. 1(236), 84–107, 2016