Automated Reasoning for Verification

Errors in hardware and software cost millions of pounds to industries and can lead to loss of life. Verification is aimed at ensuring that hardware and software are error-freeand at helping to debug existing systems. Automated reasoning plays a central role in verification since it provides efficient automated methods for formally proving that systems are functioning correctly and tools for finding errors. Our research group is world-leading in automated reasoning and our reasoning systems are regularly winning major divisions of the World Championship of Automated Theorem Proving (CASC). We are actively collaborating with Intel and Microsoft
on applications of reasoning methods into verification of hardware and software.

Automated reasoning is a thriving and exciting area which is full of challenges ranging from theoretical problems to efficient implementation and practical applications.

* Theoretical challenges include: developing efficient reasoning methods for logics used in verification such as linear and non-linear arithmetic, bit-vectors and arrays; decision procedures for combination of theories; model finding; invariant generation; integration of specialised reasoning with first-order reasoning.

* Implementation challenges: developing new algorithms, datastructures, indexing techniques and optimisations, scalable to real-life problems.

* Application challenges: methods for encoding verification problems into logics and their fragments and optimisations of general methods towards practical problems. There are exciting opportunities of applying developed methods to challenging real-life verification problems working in collaboration with Intel and Microsoft.


There are a number of PhD projects available addressing these challenges. Depending on the student’s interests, the focus of the project can be more theoretical or more implementation and application oriented.

Requirements: strong interest in logic, formal methods, and willingness to implement and experiment with new ideas.