Skip to content
Research Fellows Directory

Konstantin Korovin

Dr Konstantin Korovin

Research Fellow


University of Manchester

Research summary

In recent years there has been rapid growth in the complexity of engineering and information systems. For example, modern micro-processors contain many millions of transistors and are used extensively in computers, mobile phones, trains and power plants. Moreover, most safety-critical applications such as nuclear power plant control, air-traffic control and railway systems rely heavily on correct functioning of such complex devices, likewise on correct functioning of the software which operates these devices.

Automated reasoning aims to provide powerful tools for coping with the increasing complexity of hardware and software systems. The importance of reasoning methods has triggered many developments which interconnect research areas ranging from computer science to mathematics and engineering.

During my URF, I have been developing a novel approach to automated reasoning, which is called instantiation

generation (Inst-Gen). One of the main advantages of this approach is that it is based on expressive first-order logic, which allows one to apply Inst-Gen to a wide range of applications. Inst-Gen also incorporates powerful low-level reasoning technologies which are crucial for scalability into industrial-size problems. My work covers advanced theoretical methods, efficient reasoning algorithms and applications of automated reasoning. Based on my theoretical results, I developed and implemented a reasoning system called iProver. iProver is a world leading system in its class and has won the major EPR division at the annual world championship of automated reasoning systems

(CASC) each year since 2008. In 2012 iProver also won the satisfiability division (FNT) at an international competition CASC@Turing. This is the first time a UK based system won the FNT division. iProver has developed rapidly from an academic system into an industrial-strength tool. This is demonstrated by my current collaboration with Intel where iProver is used for hardware verification.

Grants awarded

Automated Reasoning for Complex Systems

Scheme: University Research Fellowship

Dates: Oct 2012 - Sep 2015

Value: £277,571.04

Automated Reasoning with Concrete Domains

Scheme: University Research Fellowship

Dates: Oct 2007 - Sep 2012

Value: £418,522.86