| EPSRC Reference: |
GR/L90538/01 |
| Title: |
A SUBSTRUCTURAL LOGIC FOR FORMAL VERIFICATION |
| Principal Investigator: |
Kalvala, Dr S |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Warwick |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 September 1998 |
Ends: |
31 August 2001 |
Value (£): |
52,028
|
| 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 |
|
Theorem provers have been used extensively for verification of software and hardware. Their use in formal verification is limited by the practical difficulty of modelling large representational systems in low-level mathematical notations. When general-purpose logics are used to embed application-specific formalisms, explicit manipulation of changing state results in verbose descriptions cluttered by unnecessary detail. Therefore they need to be enhanced in some way to provide a clear and amenable mechanism for keeping track of changing values. This limitation will be addressed by exploiting recent results in the study of substructural logics, such as Linear Logic, which naturally address some of the problematic issues in the use of more traditional logics. The aim of the project is to define a substructural logic which is suitable for representing the kind of information which arises in the verification cycle.The resulting logic will serve as a basis for a tool for specification and verification of dynamic systems. Rather than creating a completely new system, as in related work, we will build on the existing `Isabelle' generic theorem prover. The advantage of this is that Isabelle provides a well-developed proof interface and is extensively known and used by the verification community.
|
|
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.warwick.ac.uk |