Konstantin Korovin's Homepage

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

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

Teaching:

Automated Reasoning and Verificatinon COMP60332 (2014/2015) (with Renate Schmidt) Intro Talk for Reasoning and Optimisation theme
Automated Reasoning and Verificatinon COMP60332 (2013/2014) access via Blackboard
Logic and Modelling COMP21111 (2012/2013) Access via BlackBoard; previous year
Logical Reasoning and Applications COMP61111 (2011) (with Renate Schmidt)
Logic and Applications COMP61111 (2010) (with Renate Schmidt)
Logic in Computer Science CS2142

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

Related searches:
reasoning korovin science school schmidt

gipoco.com is neither affiliated with the authors of this page or responsible
for its contents. This is a safe-cache copy of the original web site.

gipoco.com is neither affiliated with the authors of this page nor responsible for its contents. This is a safe-cache copy of the original web site.