Verified Software Initiative (VSI)

It is estimated that faulty software costs the world economy in the order of 100 billion dollars yearly. Hence, efforts that can be made to help improve software reliability, even in a small way, will be worthwhile. We have at our disposal unprecedented computing power and we have been witness to important advances in the theories underlying programming as well as the capabilities of automated theorem provers. It is with this backdrop that in 2003 Sir Tony Hoare determined that the “time was right” to revive Robert Floyd’s 1967 Verifying Compiler (VC) project. Hoare and other eminent researchers in the field, recast the project in the form of a Grand Challenge for Computer Science and Software Engineering known as Grand Challenge 6 (GC6), Dependable Systems Evolution. More recently, the GC6 has lead way to the Verified Software Initiative (VSI).

In summary, the VSI is an international effort with a time scale of 15-20 years whose main deliverables consist of:

• Unified theory of software analysis and construction, encompassing modern programming paradigms such as object-orientation as well as concurrent programming;
• tools embodying the theory, in particular the Verifying Compiler (VC), a tool that can establish the correctness of a program, relative to its specification, before it is run;
• Verified Software Repository (VSR) of (verified) industrial grade applications and their specifications.

The overall goal of the DSRG is to contribute to the development of theories, languages, tools and methodologies that can help the software industry be more effective at developing quality software. While there are many possible research avenues, we seeking to achieve this goal through research on

• Verification Centric Software Engineering (VCSE) in general, and
• Behavioral Interface Specification Languages (BISLs) in particular.

Java Modeling Language

We are currently focusing our research efforts on the Java Modeling Language (JML), a BISL for (sequential) Java. Java makes for an interesting base research language not only because it is tractable (as compared to, say, C++), but also widely used in industry, particularly in security and safety critical areas such as Web-based Enterprise Applications (WEAs) and embedded devices and controllers (such as smart cards, avionics and aerospace devices). It is clear that overall, safety and security in software applications will require a combination of several approaches, we believe that BISLs are one effective approach to detecting and helping prevent errors.

The DSRG has made and plans to continue making contributions to:

• Improving the language design and strengthening the semantic foundations of JML.
• Verification tools: enhancing and consolidating into a new infrastructure. To this end we are developing Eclipse-based infrastructures, named JmlEclipse (formerly JML4), designed to support Runtime Assertion Checking (RAC), Extended Static Checking (ESC), and Full Static Program Verification (FSPV).
• JML case studies which we hope to submit to the GC6 Verified Software Repository.

SparkAda

We have have recently joined SAnToS Lab members to contribute to the language and tool evolution of SparkAda, a BISL for a subset of the Ada programming language.