Invited Speaker

Jump to: navigation, search

FMOODS & FORTE Invited Speaker


FORTE traces its heritage back to the Protocol Specification, Testing and Verification (PSTV) conference first held in 1981 at Teddington, UK. Since that first meeting, PSTV has evolved into FORTE, and this year's conference in Amsterdam is the 30th meeting in the conference series. To highlight this milestone, this year's DisCoTec plans to include a special celebration reflecting on the progress of the community since 1981 and challenges for the future.

In the first PSTV meeting in 1981, Gerard Holzman published a paper containing his early views of what would become the SPIN model checker. We are pleased to note that special work in the history of FORTE by featuring Dr. Holzmann as the keynote speaker of FORTE 2010 as part of this special celebration of FORTE's history.

Keynote Speaker:Gerard Holzmann, Jet Propulsion Laboratory, USA

Title: Formal Software Verification: How Close Are We?

Abstract

Spin and its immediate predecessors were originally designed for the verification of data communication protocols. It didn't take long, though, for us to realize that a data communications protocol is just a special case of a general distributed process system, with asynchronously executing and interacting concurrent processes. This covers both multi-threaded software systems with shared memory, and physically distributed systems, interacting via network channels.

The tool tries to provide a generic capability to prove (or as the case may be, to disprove) the correctness of interactions in complex software systems. This means a reliable and easy-to-use method to discover the types of things that are virtually impossible to detect reliably with traditional software test methods, such as race conditions and deadlocks.

As initially primarily a research tool, Spin has been remarkably successful, with well over one million downloads since it was first made available by Bell Labs in 1989. But our goal is te development of a tool that is not only grounded in foundational theory, but also usable by all developers of multi-threaded software, not requiring specialized knowledge of formal methods.

In this talk we try to answer the question how close we have come to reach these goals, and where especially we are still lacking. We will see that our understanding has changed of what a verification tool can do -- and what it should do.

DisCoTec2010
COORDINATION
Personal tools