| 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: |
|
| 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: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
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
|
|
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.sussex.ac.uk |