EPSRC logo

Details of Grant 

EPSRC Reference: EP/K023837/1
Title: Logical Relations for Program Verification
Principal Investigator: Ghani, Professor N
Other Investigators:
Researcher Co-Investigators:
Project Partners:
IT University of Copenhagen Microsoft University of Edinburgh
Department: Computer and Information Sciences
Organisation: University of Strathclyde
Scheme: Standard Research
Starts: 30 September 2013 Ends: 29 September 2017 Value (£): 442,444
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
16 Jan 2013 EPSRC ICT Responsive Mode - Jan 2013 Announced
Summary on Grant Application Form
In an economy as relentlessly digital as the modern worldwide one, in

which everything from toasters to interpersonal communications to

global financial services are computerised, the need for formally

verified software cannot be overestimated. Formal verification uses

mathematical techniques to prove that programs actually perform the

computations they are intended to perform (e.g., that text editors

really do save files when a SAVE command is issued or that automatic

pilots really do correctly execute flight plans) and also avoid

performing unintended ones (e.g., leaking credit card details or

launching nuclear weapons without authorisation). Since programmers

make 15 to 50 errors per 1000 lines of code, and since repairing them

accounts for some 80% of project expenses, the ever-increasing size

and sophistication of programs makes formal verification increasingly

critical to modern software development.

Mathematical reasoning lies at the core of all formal verification,

and so is crucial for building truly secure and reliable software.

One of the key techniques for formally verifying properties of

software systems uses logical relations. Logical relations provide a

means of deriving properties of a software system directly from the

system itself; as a result, they can be used to prove important

properties of programs, programming languages, and language

implementations. Logical relations have been developed for core

fragments of many modern programming languages and verification

systems. They are currently extended to richer programming languages

and properties by constructing plausible variants of the definitions

of logical relations for appropriate core fragments and checking that

the mathematical theory goes through. But as languages and properties

to be proved have become increasingly sophisticated and expressive,

this ad hoc approach has become both difficult and unsustainable. It

has also led to an enormous constellation of complicated and

non-reusable logical relations that "work" for particular language

features, rather than their principled and transferrable development

from fundamental principles. In short, logical relations have

struggled to keep pace with developments in programming languages,

with the obvious consequences for security and reliability of software


We aim to revolutionise the landscape of logical relations by

providing framework for their development and use that is principled,

conceptually simple, reusable, and uniform (rather than ad hoc). Our

framework will be capable of both describing the wide array of logical

relations already used in existing applications and prescribing new

logical relations for future ones. It will be based on the

mathematical concept of comprehension for a fibration, which has not

previously been identified as a key ingredient in

the construction of logical relations. Our use of it thus

distinguishes our framework from all other treatments of logical

relations in the literature. Comprehension allows explicit representation of logical properties of

languages within those languages themselves. This means that our

framework will be implementable, so we will produce a logic for

deriving consequences of logical relations and a prototype

implementation of that logic in a modern interactive theorem

prover. This will allow users to experiment with our framework, and

allow their experiences with it to feed back into its

foundations. We will also apply our new framework for logical

relations to cutting-edge problems that are the focus of active

research and for which there is presently no consensus on the way

forward. Successful application of our framework will show that it can

solve problems that are the focus of active research, as

well as open up unanticipated new research directions. Conversely, the

practical applications we pursue will raise challenges that prompt us

to further refine its foundations
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
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.strath.ac.uk