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


  • 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