Konstantin Korovin's photo

Homepage of Konstantin Korovin

[2007-currently] 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.
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
iProver's Prizes iProver won in 2014/2013:
* First-order satisfiability division (FNT) at CASC-J7/ CASC-24
* Effectively propositional division (EPR) at CASC-J7/ CASC-24

iProver won in 2012:
* FNT division at CASC@Turing
* EPR division at CASC@IJCAR

PhD opportunities: 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 UK and EU PhD students.


REVES: REasoning in VErification and Security

Ph.D. Christoph Sticksel (co-supervised with Renate Schmidt) graduated 2011, congratulations Christoph!!!
MSc. Ahmad Abu-Khazneh (graduated 2007)

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

PC member of: 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