Formal Methods Day
Department of Computer Science - 30th anniversary year (1997-98)

27 November 1997

The first of a series of one-day colloquia organised by the research groups in the Department

Speakers:
Prof Samson Abramsky, Department of Computer Science, University of Edinburgh:
Completing Strachey's Programme: towards a mathematical theory of realistic programming languages

Abstract: In his pioneering work on denotational semantics, summarized in his 1976 monograph with Robert Milne, A Theory of Programming Language Semantics, Christopher Strachey mapped out a programme of giving a precise mathematical account of the semantics of a wide-spectrum modern programming language, as a basis for a rigorous approach to software engineering. One formulation of this in current terms is: to give a fully abstract semantics for languages such as Standard ML. The underlying aim is to give a definitive analysis of concepts such as procedures, references and local state, continuations and exceptions, which are at the core of today's programming languages, including object-oriented languages such as Java. This version of Strachey's programme has seemed well out of reach for the 20 years following the publication of his monograph. Capturing the semantics even of the functional fragment in a precise way eluded many attempts; and dealing properly with non-functional features such as local state seemed to present significant additional problems. However, the situation has changed following recent progress in a novel approach to semantics based on modelling computation as a game, in which a system interacts with its environment like a player pitting his wits against an adversary. There is now a real prospect of completing (this version of) Strachey's programme. The key ideas of games semantics will be presented informally, and the progress towards completing Strachey's programme, and some key issues for future research, will be discussed.
Dr Bent Thomsen, ICL, Research & Advanced Technology, Group Technical Directorate:
Mobile Agents, Facile and Theory of Computing

Abstract: Mobile agents, i.e. pieces of programs that can be sent around networks of computers, are starting to appear on the Internet. Such programs may be seen as an enrichment of traditional distributed computing. Since mobile agents may carry communication links with them as they move across the network, they create very dynamic interconnection structures that can be extremely complex to analyse. In this talk we give a short introduction to mobile agents, discuss their potential and describe a proof-of-concept implementation called Mobile Service Agents. Mobile Service Agents are written in the Facile language. Facile's basis on formal process models for mobility (e.g., the pi-calculus and CHOCS) and on functional programming languages makes the language well suited for developing a significant class of mobile applications. We discuss how advanced semantic concepts such as advanced type systems, true concurrency, causality and locality can be used to analyse Mobile Agent based systems. Finally we discuss challenges that Mobile Agents bring to Theory of Computing.
Dr Gerard J Holzmann, Computing Principles Research Dept, Bell Labs, Murray Hill, NJ, USA:
Proving properties of concurrent systems: The theory and practice of a model checker

Abstract: The development of any non-trivial piece of software is an intellectually challenging task. This much has been known for as long as computers have existed. The question still is what we can do about this. In the sixties and seventies our attempt was to develop a new discipline of programming, and new proof techniques that would allow us to attain reliable software by construction. But the complexity of computer systems increases much more rapidly then our ability to understand and control them. And also today, buggy software is still very much a fact of life. In this talk I'll describe a different attempt to confront this crisis. We consider the construction of a piece of software as just another engineering task. The task is most constructively handled by a technique that is borrowed from other engineering disciplines: by prototyping and model building. A model is an abstraction of a planned system that has the advantage that it can be analyzed thoroughly for its intended and unintended design characteristics. Considerable practical experience with this style of model checking for hardware and software components has been gained in the last few years. I'll discuss the theoretical basis for an efficient on-the-fly model checking system that supports this style of software design, and will discuss some recent applications.

back