Joint CAV/ISSTA Special Event on Specification, Verification, and Testing of Concurrent Software
Wednesday, 14 July 2004
5.30pm-7.30pm

Concurrency is ubiquitous in modern software.  The computing base of systems software, comprising operating systems and databases, has always been highly concurrent. With the introduction of language-level thread primitives in Java and C# and the advent of distributed web services, concurrency has become commonplace even in application software.  The application programmer of today deals with concurrency issues just as much as the systems programmer of yesterday.

The design of concurrent software is notoriously error-prone due to the nondeterministic interaction among concurrently executing threads.  Therefore, it is important to develop techniques for specifying correctness properties of concurrent software and tools for automatically checking these properties.  This event seeks to bring together researchers who are interested in developing such techniques and tools.  To improve the reliability of concurrent software, a variety of analysis techniques are required, both static such as model checking, program analysis, theorem proving and type systems, as well as dynamic such as run-time analysis and testing. A goal of this event is to generate discussion among researchers who have traditionally worked on different analysis techniques.  We hope that this discussion will lead to collaboration for creating powerful combinations of these techniques.

To stimulate and focus discussion, this event will revolve around the concrete problem of specifying and verifying Daisy, a file system written in about 1KLOC of Java. Daisy is highly concurrent with fine-grained locking but it uses simple data structures.  In the first part of the event, invited speakers will give short talks about the use of their favorite technique to validate Daisy.  The event will conclude with an open discussion of the advantages and disadvantages of the various techniques and of ways to fruitfully combine them.

The source code of Daisy is available for download here. We encourage researchers in the area of software testing and verification to apply their prototype tools to Daisy and share their experiences with other researchers at this event.  Please send all questions about this event and Daisy to Shaz Qadeer (qadeer at_sign microsoft.com).

Five groups presented the results of applying their testing/verification technique to Daisy.  Here are the slides for the various presentations.