EPSRC logo

Details of Grant 

EPSRC Reference: EP/H010815/1
Title: jStar: making java verification practical
Principal Investigator: Gordon, Professor M
Other Investigators:
Parkinson, Dr M
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 DatePanel NameOutcome
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
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
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