Research Fellows Directory
Dr Konstantin Korovin
University of Manchester
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.