Resource Static Analysis
Lead Research Organisation:
University of Edinburgh
Department Name: Sch of Informatics
Abstract
Software systems and computer networks are prone to failure. The National Institute of Standards and Technology estimates software errors cost the U.S. economy $59.5 billion annually. It is likely that costs in Europe are on a similar scale.Static Analysis is a technique for analysing software without executing it, to help detect and repair defects. With increasing complexity of software, traditional testing and validation techniques are stretched to the limit. Automated static analysis tools look set to become a crucial part of modern software development. We will build 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. This Follow-on Fund project aims to capitalise on a ground-breaking strand of research supported by EPSRC funds since 2000, set in a wider background of over 40 years of world-leading research in Types, Logic, and Theorem Proving at the University of Edinburgh, much of which was also funded by EPSRC and its predecessors.
Publications
Atkey R
(2009)
Algebra and Coalgebra in Computer Science
Atkey R
(2011)
Amortised Resource Analysis with Separation Logic
in Logical Methods in Computer Science
Da Silva L
(2023)
Antibacterial potential of chalcones and its derivatives against Staphylococcus aureus.
in 3 Biotech
Fenacci D
(2011)
Static Resource Analysis for Java Bytecode Using Amortisation and Separation Logic
in Electronic Notes in Theoretical Computer Science
Helfenstein J
(2022)
An approach for comparing agricultural development to societal visions.
in Agronomy for sustainable development
| Description | A prototype program analysis 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. |
| Exploitation Route | Some of the general techniques for resource analysis of software programs continue to be applicable to a range of domains, e.g., cyber security. |
| Sectors | Aerospace Defence and Marine Digital/Communication/Information Technologies (including Software) Energy |
| URL | http://groups.inf.ed.ac.uk/resa/ |
| Description | The main use was the further investigation in the University R&D and spin-out company Contemplate Ltd. Some of this technology is now being used in industry to help build higher quality software that suffers from fewer unpredictable failures, or flaws that can be exploited by cyber attackers. |
| First Year Of Impact | 2012 |
| Sector | Digital/Communication/Information Technologies (including Software),Financial Services, and Management Consultancy |
| Impact Types | Societal Economic |
| Description | ITI Techmedia |
| Organisation | ITI Techmedia |
| Country | United Kingdom |
| Sector | Private |
| Start Year | 2009 |
| Company Name | Contemplate |
| Description | Contemplate develops tools that analyse large amounts of code and detect faults in them. Their first product ThreadSafe focuses on finding concurrency faults and is used in the financial sector. |
| Year Established | 2009 |
| Impact | Contemplate sells the tool ThreadSafe, which is the only commercial quality static analysis tool dedicated to finding concurrency bugs in enterprise scale Java programs. It has been used by some of the top ten investment banks in the world to find flaws in their systems which could have resulted in disasterous failures. |
| Website | http://www.contemplateltd.com |