Konstantin Korovin's photo

Homepage of Konstantin Korovin

[2015-currently] Senior Lecturer, School of Computer Science, The University of Manchester.
[2007-2015] Royal Society University Research Fellow and Lecturer at School of Computer Science, The University of Manchester.
[2014-currently] Programme Director for Master of Research (MRes)
[2004-2007] Research associate at the University of Manchester.
[2005] Ackermann Award
[2003-2004] Researcher at the Max-Planck-Institut für Informatik, Saarbrücken, Germany.
[2003] PhD degree from the University of Manchester, School of Computer Science, Supervisor Andrei Voronkov.

Research interests: iProver --- a theorem prover for first-order logic with support for arithmetical reasoning.
New release iProver v3.5 (SMT-COMP 2021/CASC-28) is available now.
iProver has been winning major divisions at The World Championship for Automated Theorem Proving (CASC)
  • automated theorem proving
  • solving non-linear constraints
  • machine learning for automated theorem proving
  • quantified Boolean logic
  • verification of hardware and software
  • first-order logic
  • instantiation-based reasoning
  • combination of theories and reasoning methods
  • DNA computing
iProver's Prizes iProver won in 2019, 2018, 2017, 2016:
* Effectively propositional division (EPR) at CASC-j9
* Effectively propositional division (EPR) at CASC-26
* Effectively propositional division (EPR) at CASC-J8
iProver: 2nd place in DQBF 2018: QBF-Eval 2018
iProver won in 2014 and 2013 at CASC-J9
* First-order satisfiability division (FNT) at CASC-J7 and CASC-24
* Effectively propositional division (EPR) at CASC-J7 and CASC-24

PhD positions: If you are interested in any of the topics above and would like to apply for a PhD, please email me: konstantin.korovin@manchester.ac.uk.
Funding is available on a competitive basis.


KSMT solver for solving non-linear constratins including trigonometric functions (see, papers and slides ).
Best Paper Award: at The 12th International Symposium on Frontiers of Combining Systems (FroCoS'19)
PC member of: CADE-27, AITP'19, SC-square'19, PSI'19, IJCAR-2018, CADE'17, PSI'17, VMCAI'17, PAAR'16, IWIL'15, HCVS'15, IJCAR'14, PSI'14, QUANTIFY'14, HCVS'14, PAAR'14,CADE'13, SYNASC'13, IWIL'13, PxTP'13, UNIF'13, IJCAR'2012, UNIF 2012, PAAR 2012, LPAR-18 (2012), IWIL 2012,FTP'2011, LPAR-17, LPAR-16, IWIL'2010, LPAR'09, RTA'08, PAAR'08, LPAR'07

Invited talks: LaSh'19, PRUV'18, Dagstuhl'18, Big Proof (Isaac Newton Institute, Cambridge) 2017, Dagstuhl'16, LaSh'14/QUANTIFY'14, FroCoS'13, Dagstuhl'12, Collegium Logicum 2011, Ringberg'11, Intel, CADE-22 (09), ARW'09, IWIL'06

Summer school: SAT/SMT/AR (2019), Lisbon slides
Summer school: Verification Technology, Systems & Applications (VTSA'2013), slides part 1, slides part 2.

SAT/SMT/AR/Computer Algebra Summer School in Manchester 3-6 July 2018

Intel: verification and optimisation of systems modelled using machine learning
SCorCH: Secure Code for Capability Hardware
Soteria: Research and development for cyber security
REVES: REasoning in VErification and Security

Co-chair of: Satisfiability Checking and Symbolic Computation (SC^2), 2020, ANDREI-60,IWIL-18, UNIF'13, IJCAR'12, IWIL'12, UNIF'12

PostDoc/PhD/MPhil Students:
Hard Reality Tool --- HRT is a tool for randomly extracting hard and realistic theory problems (conjunctive constraints) from SMT problems with a non-trivial boolean structure. GoRRiLA is another tool for randomly generating (i) linear arithmetic problems and (ii) propositional problems.

School of Computer Science
University of Manchester
Oxford Road
Manchester M13 9PL
Kilburn building, room number 2.40
e-mail: konstantin.korovin@manchester.ac.uk
phone: +44-161-3067005 (work)
fax: +44-161-275-6204

Konstantin Korovin