| EPSRC Reference: |
EP/C520726/1 |
| Title: |
Numerical Domains for Software Analysis |
| Principal Investigator: |
Hill, Dr PM |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Computing |
| Organisation: |
University of Leeds |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 February 2005 |
Ends: |
31 January 2006 |
Value (£): |
49,727
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Guaranteeing the reliability, trustworthiness, safety and security of hardware and software systems is a major challenge; erroneous behavior of computer systems can have catastrophic consequence. Static analysis provides a systematic way of determining correct though approximate information about the behavior of a system. When built on the formal framework of abstract interpretation, statice analysis offers a rigor not provided by testing and simulation, with a scalability out of reach of methods based on exhaustive checking of concrete models or verification using automated theorem proving. Many important program properties involve large or infinite sets of states or relations between these sets. In static analysis, these properties are represented and propagated by abstract domains and operations on these domains.In this project, we are concerned with investigating abstract domains that can capturing numerical information about a program's computational behavior (for instance, the possible numerical values of a program variable or the length of a dynamically allocated buffer).Previously, there has been considerable research and development of polyhedral domains and various simple special forms of these domains. Note that, an element of the domain of convex polyhedra is a convex region of n-dimensional space that can be described by means of a finite systems of linear constraints (equalities and inequalities). Then any point in such a region can denote a possible vector of values that a program's attributes (such as its variables) can take. More recently, there has been some interest and new research into domains such as the domain of integral lattices (called here 'grids') that can characterise the discrete distribution of these attributes' values in the same n-dimansional space. However, it has been shown that for accurate analysis of real applications software, we need a combination of discrete and continuous domains to represent the different kinds of program attributes and the complex relations that can hold between them.This project will) therefore study a range of new generic domains that can capture a combination of two kinds of numerical information, representing the both the distributions of the values and convex information that represents the outer limits of the values. It will study a variety of approaches for combining the existing domains of polyhedra with the new domain of grids leading to generic hybrid domains that can be used in analyzers to help in developing reliable, safe and dependable software.
|
|
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.leeds.ac.uk |