EPSRC logo

Details of Grant 

EPSRC Reference: EP/R001758/1
Title: Efficient Software Verification by Reasoning about Abstractions
Principal Investigator: Schrammel, Dr P
Other Investigators:
Researcher Co-Investigators:
Project Partners:
DiffBlue Ltd Programming Research Ltd
Department: Sch of Engineering and Informatics
Organisation: University of Sussex
Scheme: First Grant - Revised 2009
Starts: 01 August 2017 Ends: 31 January 2019 Value (£): 99,279
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
01 Jun 2017 EPSRC ICT Prioritisation Panel June 2017 Announced
Summary on Grant Application Form
Software is at the core of our daily lives. However, developing high-quality software we can rely on with confidence is challenging. Automated software verification technology has made tremendous progress in recent years. For example, current tools allow us to prove the absence of crashes (so-called runtime errors) in avionics flight software fully automatically, reducing the need for expensive testing. The key challenge in verification is finding the right compromise between two conflicting goals: scalability and precision. These are the key problems that hinder more widespread adoption of automated verification technology: lack in scalability prevents verification technology from being applied to large software bases, such as enterprise software; and lack in precision makes it impossible to verify, for example, full functional specifications that do not only ensure that the auto-pilot software does not crash, but also that it behaves correctly in dangerous situations.

The key concept that enables compromises between scalability and precision is abstraction, i.e. leaving out unnecessary detail while still being able to give guarantees about the system's behaviour. Current techniques use either pre-defined abstractions (so-called abstract domains) that target specific kinds of properties, e.g. absence of runtime errors; designing such abstractions is a tedious manual process. Or they use abstraction refinement techniques, which automatically search for a suitable abstraction within a restricted set of options (e.g. fragments of first-order theories) chosen by the tool designer. Moreover, these techniques are often heuristic, which affects their robustness.

This project proposes a way out of this impasse by developing a scalable, systematic approach to finding the right abstractions on a higher level, thus reducing the need of user or design time decisions. This involves developing a theoretical framework for abstraction inference and search that builds on existing abstraction theory. Whereas such a framework has applications in many areas, we will devise efficient algorithms in particular for the application of software verification, implement them and demonstrate the power of the approach on representative software verification problems and industrial case studies from the embedded systems and enterprise software domain.

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.sussex.ac.uk