Page d'accueil // SnT // Distinguishe... // Abstraction as a Unifying Link for Formal Approaches to Concurrency - November 22, 2012

Abstraction as a Unifying Link for Formal Approaches to Concurrency - November 22, 2012

It is our pleasure to host this distinguished lecture by Prof. Cliff Jones, Newcastle University. The lecture will be followed by a reception. Please feel free to forward this invitation.

Date: November 22, 2012
Time: 16:30
Venue:  Weicker Building -Room B001 Ground floor, 4 rue Alphonse Weicker, L-2721 Luxembourg

Abstract: This talk presents the case for careful use of abstractions that can make it easier to marry the advantages of different approaches to reasoning about concurrency. Abstraction is a crucial tool in specifying and justifying developments of systems. This observation is recognised in many different methods for developing sequential software; it also applies to some approaches to the formal development of concurrent systems. The rely/guarantee approach to formal design has, for example, been shown to be capable of recording the design of complex concurrent software in a ``top down'' stepwise process that proceeds from abstract specification to code. In contrast, separation logics were motivated by reasoning about details of extant code. Such approaches can be thought of as ``bottom up''. Some useful mixes of these approaches already exist and they are not to be viewed as competitive approaches. In fact, abstraction is the key ingredient to provide practical links.

Dr. Cliff Jones is Professor of Computing Science at Newcastle University. He is best known for his research into "formal methods" for the design and verification of computer systems; under this heading, current topics of research include concurrency, support systems and logics. He is also currently applying research on formal methods to wider issues of dependability. Running up to 2007 his major research involvement was the five university IRC on "Dependability of Computer-Based Systems" of which he was overall Project Director - this was followed by a  Platform Grant  "Trustworthy Ambient Systems" (TrAmS / TrAmS-2. He also coordinated the work packages on methodology in the DEPLOY project. He currently runs the EPSRC-funded AI4FM project.

As well as his academic career, Cliff has spent over twenty years in industry (which might explain why "applicability" is an issue in most of his research). His fifteen years in IBM saw, among other things, the creation -with colleagues in the Vienna Lab- of VDM which is one of the better known "formal methods". Under Tony Hoare, Cliff wrote his Oxford doctoral thesis in two years. From Oxford, he moved directly to a chair at Manchester University where he built a world-class Formal Methods group which -among other projects- was the academic lead in the largest Software Engineering project funded by the Alvey programme (IPSE 2.5 created the "mural"(Formal Method) Support Systems theorem proving assistant).

During his time at Manchester, Cliff had a 5-year  Senior Fellowship  from the research council and later spent a sabbatical at Cambridge for the whole of the Newton Institute event on "Semantics". Much of his research at this time focused on formal (compositional) development methods for concurrent systems for which he has just received another four-year research grant. In 1996 he moved to Harlequin, directing some fifty developers on Information Management projects and finally became overall Technical Director before leaving to re-join academia in 1999.

Cliff is a  Fellow  of the Royal Academy of Engineering (FREng), ACM, BCS, and IET. He has been a member of IFIP Working Group 2.3 (Programming Methodology) since 1973 (and was Chair from 1987-96).