Verification-centric Software Engineering

A GLOBAN Summer School Course

Date: 22-23 September 2008
Location: Institute of Informatics, University of Warsaw, Warsaw, Poland

Instructor: Joe Kiniry

Tutorial materials prepared with the able assistance of: David Cok, Fintan Fairmichael, Gary Leavens, Erik Poll, and Dan Zimmerman

Abstract

This series of talks focus on the practical aspects of designing, constructing, and validating global computing software systems. A suite of robust academic tools, many of which were developed under the EU FP6 MOBIUS project, which are part of the MOBIUS Program Verification Environment (PVE), are summarized and demonstrated.

The first talk gives an overview of the tools options available today, including tools used in this series of talks and others. The second talk focuses on the practical aspects of designing systems for verification. The third talk focuses on refining designs into implementations and validating those designs and refinements via various static checking techniques and automated testing. The final talk focuses on using interactive and automatic theorem provers to perform full functional verification.

Participants are given the latest release of the MOBIUS PVE and other related tools on a CD-ROM or USB key.

Attendee Background

Any Java programmer who wishes to improve the quality of their software should attend. Also, educators who want to use BON, JML, and/or ESC/Java2 in teaching, as a gentle way to introduce students to state-of-the-art specification and verification techniques and tools supporting formal methods, should also attend this tutorial.

Objectives

Attendees will come out of this tutorial with a firm understanding of the use of specifications in software design and engineering, a basic knowledge of the BON and JML specification languages, and will be knowledgeable about the various tools available for the BON and JML languages, particularly BONc and ESC/Java2.

Tutorial History

Variations of this tutorial have been presented to over a hundred academics and several hundred undergraduate and postgraduate students over the past several years. The first version of this tutorial was one of the most successful tutorials at ECOOP 2004. Extensive slides, homework assignments, and an ongoing book on JML and ESC/Java2 are available. Alternate versions of this tutorial have also been given at several other top academic conferences, including ECOOP, ETAPS, FM, TOOLS, and FMCO.

Biography

Joseph Kiniry, University College Dublin
Joe is a lecturer in the School of Computer Science and Informatics at University College Dublin. He was previously in the SoS Group at Radboud University Nijmegen. He earned his Ph.D. in Computer Science from the California Institute of Technology. Joe is the coauthor of ESC/Java2 and has contributed to, or led the development of, several other verification tools including BONc, FreeBoogie, Simplify, Fx7, the JML tool suite, PVS, the LOOP compiler, and, of course, the Mobius PVE.

Registration

Please see the main GLOBAN website for how to register for the Summer School.

Slides

The slides presented in this tutorial are here:

Exam

The exam for this course is included in the following workspace in the project named GLOBAN. This workspace also includes many of the examples discussed in the GLOBAN slides and in past tutorials.

Resources

The following resources are available for all interested in JML and ESC/Java, whether you decide to attend our tutorial or not.