Konstantin Korovin

[2023-] Reader, Department of Computer Science, The University of Manchester.
[2015-2023] Senior Lecturer (UoM).
[2007-2015] Royal Society University Research Fellow
[2004-2007] Research associate (UoM).
[2003-2004] Researcher at the Max-Planck-Institut für Informatik, Saarbrücken, Germany.
[2003] PhD (UoM), Best Thesis Prize, Ackermann Award, Supervisor Andrei Voronkov.

Research interests:

automated theorem proving
comination of machine learning and automated theorem proving
analysis and optimisation of machine learning models
verification of hardware and software
solving non-linear constraints
quantified Boolean logic
first-order logic
combination of theories and reasoning methods
DNA computing
Bio modelling

Please get in touch if you would like to collaborate, do projects, use or contribute to any of the tools below.

iProver --- a theorem prover for quantified first-order logic with support for arithmetical reasoning. Supported fromats: TPTP/SMT/(D)QBF/AIGER

iProver won over 20 prizes at The World Championship for Automated Theorem Proving (CASC), SMT-COMP, QBF-EVAL:

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

iProver-ML --- has a simple interface to machine learning (LPAR'23, J. Symb Comp. I, J. Symb Comp. II).
You can try your ML own model via simple interface!

SMLP

-- Symbolic Machine Learning Prover -- a system for optimization and verification of systems modelled using machine learning. SMLP is based on machine learning techniques combined with formal verification approaches that allows selection of optimal configurations with respect to given constraints on the inputs and outputs of the system under consideration.

based on SMT and Bayesian optimization.
used at Intel for optimising hardware layouts.
supports: neural networks, polynomial models, tree models
papers: CAV'24, IJCAI'22, FMCAD'20

KSMT solver for non-linear constratins including trigonometric functions.

δ-complete decision procedure for non-linear constraints.
based on a combination of comutable analysis, CDCL style reasoning and incremental linearisations.
supports: polynomial, trigonometric and general compuatable functions
papers: J. TCS'23, CADE'21, FroCoS'19 (Best paper award)
slides: ksmt sildes

Teaching:

Logic and Modelling COMP21111 (UoM)
Automated Reasoning and Verificatinon COMP60332 (UoM)
Logical Reasoning and Applications COMP61111 (UoM)
Logic in Computer Science CS2142 (UoM)

Summer Schools:

The International Summer School in SAT/SMT/AR, Manchester, co-organiser (2018)
SAT/SMT/AR Summer School in Lisbon, Portugal (2019).
International Summer School on Verification Technology, Systems & Applications, France (2013).

PhD/PostDocs/MPhil:

Ph.D. Maryam Abdullah, 2019-2025, graduated
PostDoc Kiana Samadpour Motalebi, 2024-
PostDoc Franz Brausse, 2020-2024
Ph.D. Edvard Holden, 2018-2023, graduated, ML Engineer, Elliptic Labs
Ph.D. André Duarte, 2018-2023, graduated, works at IMC Trading
Ph.D. Julio Cesar Lopez Hernandez, graduated 2020
MPhil Andrzej Kucik, graduated 2020, Research Fellow at European Space Agency (ESA), AI Research Engineer at Helsing
PostDoc Dmitri Tsarkov, 2013-2016, Senior Software Engineer at Google
Ph.D. Christoph Sticksel, graduated 2011, Principal Engineer at MathWorks

PhD opportunities:

I'm looking for PhD students, some possible projects
If you are interested and would like to apply for a PhD, please email me: konstantin.korovin@manchester.ac.uk.

Contact: konstantin.korovin@manchester.ac.uk
Connect:

Address: Konstantin Korovin
room 2.40, Kilburn building
Department of Computer Science
The University of Manchester
Oxford Road
Manchester M13 9PL
UK