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.
[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 2013:
* First-order satisfiability division (FNT) at CASC-24
* Effectively propositional division (EPR) at 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.

Publications


REVES: REasoning in VErification and Security


Students:
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: 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.

Teaching:
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.

Address:
School of Computer Science
University of Manchester Oxford Road
Manchester M13 9PL
UK
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