Konstantin Korovin's photo

Konstantin Korovin
[2023-currently] Reader, Department of Computer Science, The University of Manchester.
[2015-2023] Senior Lecturer, Department 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.
[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:
  • automated theorem proving
  • solving non-linear constraints
  • machine learning for automated theorem proving
  • analysis of machine learning models
  • quantified Boolean logic
  • verification of hardware and software
  • first-order logic
  • instantiation-based reasoning
  • combination of theories and reasoning methods
  • DNA computing
  • bio modelling
iProver --- a theorem prover for first-order logic with support for arithmetical reasoning.
New release iProver v3.7 (SMT-COMP/CASC) is available now.
iProver has been winning major divisions at The World Championship for Automated Theorem Proving (CASC)
iProver's Prizes iProver won:
* SMT-COMP single query track parallel performance (2021)
* Effectively propositional division (EPR) at CASC-j9
* Effectively propositional division (EPR) at CASC-26
* Effectively propositional division (EPR) at CASC-J8
iProver: 2nd place in DQBF 2018: QBF-Eval 2018
iProver won in 2014 and 2013 at CASC-J9
* First-order satisfiability division (FNT) at CASC-J7 and CASC-24
* Effectively propositional division (EPR) at CASC-J7 and CASC-24



Publications


I'm looking for PhD students in the following areas. If you are interested in any of the topics above and would like to apply for a PhD, please email me: konstantin.korovin@manchester.ac.uk.
Funding is available on a competitive basis. Some projects:

KSMT solver for solving non-linear constratins including trigonometric functions (see, papers and slides ).
Best Paper Award at The 12th International Symposium on Frontiers of Combining Systems (FroCoS'19)
The ksmt calculus is a δ-complete decision procedure for non-linear constraints at CADE'21.
KSMT linearisation

SMLP Optimization and verification of systems modelled using neural networks. SMLP is based on SMT and Bayesian optimization. SMLP is used at Intel for optimising parameters of analogue systems (see, our papers at IJCAI'22, FMCAD'20).
PC member of: CAV'22, AITP'22, CADE-27, AITP'19, SC-square'19, PSI'19, IJCAR-2018, 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'19, PRUV'18, Dagstuhl'18, Big Proof (Isaac Newton Institute, Cambridge) 2017, Dagstuhl'16, LaSh'14/QUANTIFY'14, FroCoS'13, Dagstuhl'12, Collegium Logicum 2011, Ringberg'11, Intel, CADE-22 (09), ARW'09, IWIL'06

Summer school: SAT/SMT/AR (2019), Lisbon slides
Summer school: Verification Technology, Systems & Applications (VTSA'2013), slides part 1, slides part 2.

SAT/SMT/AR/Computer Algebra Summer School in Manchester 3-6 July 2018

Projects:
Intel: verification and optimisation of systems modelled using machine learning
SCorCH: Secure Code for Capability Hardware
Soteria: Research and development for cyber security
REVES: REasoning in VErification and Security


Co-chair of: Satisfiability Checking and Symbolic Computation (SC^2), 2020, ANDREI-60,IWIL-18, UNIF'13, IJCAR'12, IWIL'12, UNIF'12

PostDoc/PhD/MPhil Students:
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: konstantin.korovin@manchester.ac.uk
phone: +44-161-3067005 (work)
fax: +44-161-275-6204

Konstantin Korovin