Abstracts for Invited Speakers

Analysis Is Necessary, But Far From Sufficient: Experiences Building and Deploying Successful Tools for Developers and Testers

Jon Pincus
Microsoft Research

Why are there so few successful "real-world" programming and testing tools based on academic research? This talk focuses on program analysis tools, and proposes a surprisingly simple explanation with interesting ramifications.

For a tool aimed at developers or testers to be successful, people must use it - and must use it to help accomplish their existing tasks, rather than as an end in itself. If the tool does not help them get their job done, or the effort to learn and/or use the tool is too great, users will not perceive enough value; the tool will not get significant usage, even if it is free.

This talk focuses on the often-overlooked consequences of this seemingly basic statement in two major areas: program analysis, and the work beyond core analysis that must be done to make a successful tool. Examples will be drawn from tools that have been successfully used in industry (sold commercially, and developed for internal use).

Finite State Verification: A New Approach for Validating Software Systems

Lori A. Clarke
University of Massachusetts, Amherst

Ever since formal verification was first proposed in the late sixties, the idea of being able to definitively determine if a program meets its specifications has been an appealing, but elusive, goal. Although verification systems based on theorem proving have improved considerably over the years, they are still inherently undecidable and require significant guidance from mathematically astute users. The human effort required for formal verification is so significant that it is usually only applied to the most critical software components.

Alternative approaches to theorem proving based verification have also been under development for some time. These approaches usually restrict the problem domain in some way, such as focusing on hardware descriptions, communication protocols, or a limited specification language. These restrictions allow the problem to be solved by using reasoning algorithms that are guaranteed to terminate and by representing the problem with a finite state model, and thus these approaches have been called finite state verification. Systems based on these approaches are starting to be effectively applied to interesting software systems and there is increasing optimism that such approaches will become widely applicable.

In this presentation, I will overview some of the different approaches to finite state verification. In particular I will describe symbolic model checking, integer necessary constraints, and incremental data flow analysis approaches. The strengths and weaknesses of these approaches will be described. In addition, I will outline the major challenges that must be addressed before finite state verification will become a common tool for the typical well-trained software engineer.

Progress in Testing Component-Based Software

Craig H. Wittenberg
Microsoft Research

Software components enable practical reuse of software `parts' and amortization of investments over multiple applications. Composition is the key technique by which systems of software components are constructed. However, composition yields the greatest challenges when it comes to testing, as a component-based application may be composed out of parts that were never tested together. Thus the most useful and reliable parts are those which have been tested independently in as many ways as possible. The Component Applications Group in Microsoft Research is developing tools, techniques, and a large component library to enable the development of sophisticated office, home and web-based applications. This talk will highlight our composition and specification methods, processes, and tools with a particular emphasis on our test harness and our testing results, as well as how we made use of existing testing technology and ideas. A discussion of the last few bugs found in each of several projects should prove interesting. Some comparisons will be made with other projects inside and outside Microsoft.

Model Checking Java Programs

David L. Dill
Stanford University

Automatic state exploration tools (model checkers) have had some success when applied to protocols and hardware designs, but there are fewer success stories about software. This is unfortunate, since the software problem is worsening even faster than the hardware and protocol problems. Model checking of concurrent programs is especially interesting, because they are notoriously difficult to test, analyze, and debug by other methods. This talk will be a description of our initial efforts to check Java programs using a model checker. The model checker supports dynamic allocation, thread creation, and recursive procedures (features that are not necessary for hardware verification), and has some special optimizations and checks tailored to multi-threaded Java program. I will also discuss some of the challenges for future efforts in this area.