| EPSRC Reference: |
GR/T04724/01 |
| Title: |
Program Analysis and the Pi-Calculus: Foundations and Applications to Security |
| Principal Investigator: |
Yoshida, Professor N |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computing |
| Organisation: |
Imperial College London |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 January 2005 |
Ends: |
29 February 2008 |
Value (£): |
176,053
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Logic & Combinatorics |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
This research aims at devloping a general theoretical foundation of diverse program analyses for a wide range of programming languages based on typed pi-calculus, and demonstrating their effectiveness via concrete applications. Program analysis is an increasingly important field for verifying significant properties of programs' safety, including critical security properties. So far various techniques of analysis have been developed and applied in the context of specific, and mainly sequential, programming languages and formal calculi, without a common theoretical foundation. This project aims at demonstrating how the pi-calculus with type structures coming from game semantics and linear logic can be used as a uniform technical basis for a wide range of program analyses, where the general results obtained in the theoretical calculus can be directly reflected as analyses for real programming languages such as Java. In the project, the pi-calculus with extended type structure is used as a basis for incorporating and generalising existing program analyses, including classical analyses such as control/data flow analyses and novel ones developed for various security concerns. The generalised analyses in the pi-calculus will then be reflected on to concrete languages, whose effectiveness is tested using substantial programs which include security features_ The project aims at offering a flexible and long-lasting foundation for practice, based on the expertise of the co-investigators in program analysis and the pi-calculus, extending recent successful accomplishments to a wider range of programming languages and analyses.
|
|
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.imperial.ac.uk |