Details of Grant 

EPSRC Reference:	EP/E002919/1
Title:	Linear Schemas for Program Dependence
Principal Investigator:	Danicic, Dr S
Other Investigators:	Harman, Professor M Hierons, Professor R
Researcher Co-Investigators:
Project Partners:
Department:	Computing Department
Organisation:	Goldsmiths College
Scheme:	Standard Research
Starts:	01 November 2006	Ends:	31 October 2009	Value (£):	301,452
EPSRC Research Topic Classifications:	Fundamentals of Computing Software Engineering
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:
Summary on Grant Application Form
Program schemas are a notation for representing an infinite set of computer programs all with the same syntactic structure. If a property of a program schema can be proved, this property will hold for every program in the infinite set of programs represented by the schema. Reasoning with schemas is, thus, a very powerful mechanism.As a result of their work in program slicing, the proposers found that program schema theory enabled them to precisely express the problems that they were tackling; namely the existence of statement minimal slicing algorithms at the `dataflow' level of abstraction. For such problems a class of schema which they called a `linear schema' was introduced. A linear schema is one in which no predicate or function symbol occurs more than once.Serendipitously, the proposers later discovered that the linearity condition helped in proving decidability of equivalence of schemas. Decidability of equivalence is the ability to automatically check whether two different schemas represent the same class of schemas. They proved that equivalence of conservative, free, linear schemas is decidable and later strengthened this by proving that equivalence of liberal, free linear schemas is decidable in polynomial time. This work represented significant progress in the field of schema theory after a hiatus of about thirty years. There is strong evidence that the imposition of this extra but natural condition of linearity (or partial forms of linearity) will lead to further decidability results in the theory of schemas.The proposers hope that their new results will lead to a re-appraisal of the substantial body of work in program schema theory and to further research its applications in a modern framework. This is one of the main motivations of this research proposal.Much static program transformation and analysis, in fact all analysis which uses data and control flow, takes place at the schema level of abstraction. This means the analysis of a program will produce the same results for all programs in its schema equivalence class. An important part of this research will be to investigate further the extent to which the large body of work on the theory of schemas is relevant to slicing in particular and to other forms of static program analysis and transformation in general.
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.gold.ac.uk