Preface by the section editor

The papers in this special section present a sampling of new symbolic approaches for determining whether or not a system satisfies its specification. Abstracts of these articles appeared originally in the Proceedings of the 1999 Symposium on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’99). Published online: 18 July 2001     

Using static analysis to improve automatic test generation

Conformance testing is still the main industrial validation technique for telecommunication protocols. In practice, the automatic construction of test cases based on finite-state models is hindered by the state explosion problem. We try to reduce its magnitude by using static analysis techniques in order to obtain smaller but equivalent models. Published online: 24 January 2003     

The PROSPER toolkit

The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they can be treated as components. A system incorporating such tools becomes another component that can be embedded in an application. This paper describes the software toolkit developed by the project. The nature of communication between components is specified in a language-independent way. It is implemented in several common programming languages to allow a wide variety of tools to have access to the toolkit. Published online: 19 November 2002 Work funded by ESPRIT Framework IV Grant LTR 26241. RID="*" ID="*"Michael Norrish is supported by the Michael and Morven Heller Research Fellowship at St. Catharine’s College, Cambridge. RID="**" ID="**"Konrad Slind is now at the School of Computing, University of Utah, Salt Lake City UT 84112, USA.     

Cache consistency by design

Summary. In this paper we present a proof of the sequential consistency of the lazy caching protocol of Afek, Brown, and Merritt. The proof will follow a strategy of stepwise refinement, developing the distributed caching memory in five transformation steps from a specification of the serial memory, whilst preserving the sequential consistency in each step. The proof, in fact, presents a rationalized design of the distributed caching memory. We will carry out our proof using a simple process-algebraic formalism for the specification of the various design stages. We will not follow a strictly algebraic exposition, however. At some points the correctness will be shown using direct semantic arguments, and we will also employ higher-order constructs like action transducers to relate behaviours. The distribution of the design/proof over five transformation steps provides a good insight into the variations that could have been allowed at each point of the design while still maintaining sequential consistency. The design/proof in fact establishes the correctness of a whole family of related memory architectures. The factorization in smaller steps also allows for a closer analysis of the fairness assumptions about the distributed memory.