Home page of Konstantin Korovin

Royal Society University Research Fellow at School of Computer Science, The University of Manchester.
I obtained my PhD degree from The University of Manchester, School of Computer Science, Supervisor Prof. Andrei Voronkov.

Teaching: Logic in Computer Science CS2142

Publications

iProver --- an instantiation-based theorem prover for first-order logic. New version iProver v0.7 is released!!!
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.
Students:
Ph.D. Christoph Sticksel (co-supervised with Renate Schmidt)
MSc. Ahmad Abu-Khazneh (graduated 2007)
PC member of: LPAR'09, RTA'08, PAAR'08, LPAR'07, IWIL'06
Invited Talks: CADE-22 (09), ARW'09,...
Research interests:

• Automated deduction
• Instantiation-based theorem proving
• Solving constraints in term algebras
• Computability Theory
• Model Theory

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