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 2024: ALIA, UF(24), UFNIRA
* CASC-j12 2024: FMT (SAT) division
* SMT-COMP'23: Parallel track: Eq+LinArith, Equality k
* 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:

SMLP Optimization and verification of machine learning models using symbolic methods.
  • based on SMT and Bayesian optimization.
  • used at Intel for optimising parameters of analogue systems.
  • papers: CAV'24, IJCAI'22, FMCAD'20
KSMT linearisation

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

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