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 --- an instantiation-based theorem prover for first-order logic.
New release iProver v2.6 (CASC-26, 2017) is available now.
iProver has been winning major divisions at The World Championship for Automated Theorem Proving (CASC)
  • automated reasoning
  • verification of hardware and software
  • instantiation-based reasoning
  • linear/non-linear arithmetic
  • combination of theories and reasoning methods
  • automated theorem proving
  • first-order logic
  • quantified Boolean logic
  • DNA computing
iProver's Prizes iProver won in 2017, 2016:
* Effectively propositional division (EPR) at CASC-26
* Effectively propositional division (EPR) at CASC-J8
iProver won in 2014 and 2013:
* 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: korovin@cs.man.ac.uk.
Funding is available for successful PhD applicants from the UK and EU.


REVES: REasoning in VErification and Security

Co-chair of: UNIF'13, IJCAR'12, IWIL'12, UNIF'12

PC member of: 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'14/QUANTIFY'14, FroCoS'13, Dagstuhl'12, Collegium Logicum 2011, Ringberg'11, Intel, CADE-22 (09), ARW'09, IWIL'06

Summer school: Verification Technology, Systems & Applications (VTSA'2013), slides part 1, slides part 2.

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: korovin@cs.man.ac.uk
phone: +44-161-3067005 (work)
fax: +44-161-275-6204

Konstantin Korovin