EPSRC Reference: 
EP/F067909/1 
Title: 
Expressive Multitheory Reasoning for Interactive Verification 
Principal Investigator: 
Gordon, Professor M 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Science and Technology 
Organisation: 
University of Cambridge 
Scheme: 
Standard Research 
Starts: 
01 December 2008 
Ends: 
30 November 2011 
Value (£): 
247,158

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 

Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
21 Apr 2008

ICT Prioritisation Panel (April 2008)

Announced


Summary on Grant Application Form 
As established by a panel of distinguished researchers and industrial users, Grand Challenge #6 for computer science is Dependable Systems Evolution: The vision of GC6 is of a future in which all computer systems justify the trust that society increasingly places in them. One of the key notions of what it means to be dependable is verifiability, i.e., one can guarantee that the computer system does what it is supposed to do. The highest possible level of verifiability is called formal verification , which produces a mathematical proof of a system's reliability.Formal verification for hardware and software is now widely used in missioncritical realworld applications. These include the embedded code in NASA deep space probes, the arithmetic chips in Intel and AMD CPUs, and device driver code in large consumer operating systems such as Microsoft Windows. To achieve the highest level of quality assurance, formal verification is now an essential complement to testing and simulation.Formal verification relies critically on the automation of proof methods for the mathematical theories that are used to describe systems. Automated proof can be done deductively, by proceeding via composition of simple proof rules, or nondeductively, by directly exploiting our knowledge of these theories. Nondeductive proof is fast, but the reliability of deductive proof is more obvious because it can be broken up into simple pieces.In an ideal world, nondeductive proof automation programs are used as oracles for deductive ones. The difficulty is in coming up with deductive versions of the nondeductive program's answers. Achieving a clean and useful integration of nondeductive and deductive proof automation programs is a nontrivial problem.Our research looks at proofs for a relatively new but widely deployed class of nondeductive prover programs called SMT solvers . These are specialised programs for automatically proving assertions about the behaviour of computer systems, when these assertions are expressed as mathematical formulae. We plan to augment SMT solvers to allow more complex assertions to be expressed, and then to explore methods for speeding up the deductive analysis of the answers produced by SMT solvers. Both these objectives will improve the effectiveness of industrialstrength formal verification. In this endeavour we have strong support from both industry and academia. In related previous work we achieved thousandsfold speedups in the deductive analysis of Boolean problem solvers, for the first time making deductive verification feasible for industrial Boolean problems. We have high hopes for repeating this success. Success would mean a vastly improved capability for deductive verification, and hence the ability to provide reliable highlevel qualityassurance tool kits for considerably more complicated computer systems than is currently possible.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 

Further Information: 

Organisation Website: 
http://www.cam.ac.uk 