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:
|
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) ![]() * 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 |
SMLP Optimization and verification of machine learning models using symbolic methods. |
![]() |
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. |
![]() |
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
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 |