EPSRC logo

Details of Grant 

EPSRC Reference: GR/T20106/01
Title: Formal Specification and Verification of ARM-Based Systems
Principal Investigator: Gordon, Professor M
Other Investigators:
Researcher Co-Investigators:
Dr A Fox
Project Partners:
A R M Ltd
Department: Computer Science and Technology
Organisation: University of Cambridge
Scheme: Standard Research (Pre-FEC)
Starts: 01 October 2004 Ends: 30 September 2007 Value (£): 193,684
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:  
Summary on Grant Application Form
If successful, this project will result in possibly the first machine checked formal verification of software running on a formally verified commercial offthe-shelf (COTS) processor. It will provide data and methodology to enable future system designers to evaluate the costs and benefits of formal proof of correctness as part of their verification flow. As a case study we will develop a demonstrator application written in ARM assembler that communicates over a system bus with one or more co-processors. The demonstrator will explore how mechanised reasoning can increase assurance that information is secure, a property of current commercial significance for devices like mobile phones, PDAs and set top boxes.
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
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: http://www.cl.cam.ac.uk/~acjf3/arm/
Further Information:  
Organisation Website: http://www.cam.ac.uk