Resource Static Analysis

Project Details


This was a follow-on project aiming towards moving fundamental research results closer to practical industrial application. It included technical and commerical objectives. The technical objectives of our project were to produce:

1. static analysis algorithms and annotations for resource control in Java
2. a prototype static analyser tool, equipped for resource analysis;
3. a programmer-level interface to present analysis results and assist with fixing mistakes;
4. demonstrations of our algorithms on commercially-oriented example programs.

The commercial objectives of our project were to produce:

1. a market study of application areas, market projection and customer requirements;
2. a survey of existing and anticipated competitor products;
3. a study of IP protection in the area, with a view to filing US patents;
4. relationships with end-users to exercise prototype products;
5. a commercialisation strategy plan outlining routes to market.

Layman's description

We are building a demonstration static analysis tool for Java which targets a new class of software defects not considered by existing tools: those arising from resource usage violations. Our aim is to demonstrate that resource analysis is a mature and effective technology which can be practically applied in Java program development.

Key findings

Due to a change in staff, the technical objectives of the work were modified slightly to investigate a particular combination of analysis techniques (amortised analysis and lattice-point enumeration in polytopes). A prototype engine was produced which handled small examples, including library code indicative of commercial example code.
The commercial objectives have been undertaken by Aspinall and Sannella within the spin-out company Contemplate Ltd, which is actively pursuing opportunities in closely related areas to this research, although not so far using the techniques investigated here. For the technology studied in this follow-on fund, added value dedicated support of a Business Development Executive (Richardson) was provided to pursue further connections and opportunities.
Effective start/end date1/03/0930/09/10


  • EPSRC: £126,570.00


Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.
  • Amortised Resource Analysis with Separation Logic

    Atkey, R., 2011, In: Logical Methods in Computer Science. 7, 2, p. 33 17.

    Research output: Contribution to journalArticlepeer-review

    Open Access
  • Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode

    Aspinall, D., Atkey, R., MacKenzie, K. & Sannella, D., 2010, Trustworthly Global Computing: 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers. Wirsing, M., Hofmann, M. & Rauschmayer, A. (eds.). Springer-Verlag GmbH, p. 1-22 22 p. (Lecture Notes in Computer Science; vol. 6084).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
  • Algebras for Parameterised Monads

    Atkey, R., 2009, Algebra and Coalgebra in Computer Science: Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings. Springer Berlin Heidelberg, p. 3-17 15 p. (Lecture Notes in Computer Science; vol. 5728).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution