| EPSRC Reference: |
EP/H010815/1 |
| Title: |
jStar: making java verification practical |
| Principal Investigator: |
Gordon, Professor M |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science and Technology |
| Organisation: |
University of Cambridge |
| Scheme: |
Standard Research |
| Starts: |
01 January 2010 |
Ends: |
30 September 2011 |
Value (£): |
272,173
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
02 Sep 2009
|
ICT Prioritisation Panel (Sept 09)
|
Announced
|
|
|
Summary on Grant Application Form |
|
Software is unreliable. This is a serious problem for modern society. We are in contact with software everyday, but this software often contains critical bugs. Currently, operating systems are susceptible to viruses, and commercial software packages are sold with disclaimers not guarantees. To address this, we need to develop practical verfication methods for real-world programming languages. This is about giving a mathematical specification of what the software should do, and guaranteeing the implementation meets this specification. This proposal focusses on verifying object-oriented programs. The most prominent approaches to object-oriented verification, Boogie and ESC, suffer two major problems. First, their specifications are verbose, in fact sometimes longer than the code. The reason for this is that they only support limited modularity and require redundant annotations, like many loop invariants. Secondly, their specifications are weak since they cannot express functional correctness. The problem here is that although the mantra ``say less to do more'' is alluring in the context of software specification, unfortunately, it does not work for realistic examples, or even just common design patterns. Here, we propose the following novel combination of ideas, which make practical verification for Java possible: * A separation Logic based specification language for OO giving powerful modularity. * Automatic theorem proving for substructural logics which integrates with existing theorem provers for classical logic, e.g. SMT solvers; HOL; etc. * A proof theoretic approach to abstract interpretation, which allows redundant annotations to be inferred and boost abstract interpretation to coverage of full functional correctness properties. Furthermore, we propose that all these concepts can be realised together in a unified prover/abstracter architecture.
|
|
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: |
http://jstarverifier.org/ |
| Further Information: |
|
| Organisation Website: |
http://www.cam.ac.uk |