jStar: making java verification practical

Lead Research Organisation: Queen Mary University of London
Department Name: Sch of Electronic Eng & Computer Science

Abstract

Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
 
Description Developed a new way of doing automatic program verification for
Java. This resulted in a software tool that was open sourced.
Exploitation Route It is now applied in industry.
Sectors Digital/Communication/Information Technologies (including Software)
 
Description The result of the research contributed to the main product developed by a start-up (Monoidics ltd) that me and my collaborators founded. The start-up was then acquired by Facebook and now the research developed in this grant is used daily in Facebook and other companies.
Sector Digital/Communication/Information Technologies (including Software)
Impact Types Economic
 
Title JStar: Automatic Verifier for Java 
Description JStar is a software verification tool able to verify properties expressed in separation logic for Java program 
Type Of Technology Software 
Year Produced 2010 
Open Source License? Yes  
Impact This research tool has been used in the academic community to build new research tools for software verification by other researchers 
URL http://www.jstarverifier.org
 
Company Name Monoidics 
Description Start-up developing an automatic software analyzer able to find subtle bugs in industrial software 
Year Established 2009 
Impact The company had several industrial clients using its product. Then the company was acquired by Facebook that now daily uses Monoidics software.