Skip to main content

Recent news

All news

About me

Cliff Jones

My research interests are mainly in “formal methods“. Nominal "retirement" changed little in my life: I continue to function as a Professor of Computing Science at Newcastle University (I did acquire the title of "Senior Research Investigator").

I've spent over 20 years of my career in industry. My 15 years in IBM saw the creation of VDM which is one of the better known “formal methods“. For most people, their doctoral studies are “post graduate” qualifications — but I had no degree when Tony Hoare agreed, on the basis of my publications, to supervise my doctorate. From Oxford, I moved directly to a chair at Manchester University where we built a world-class Formal Methods group. During my time at Manchester, I had a five-year Senior Fellowship funded by the research council; later I also spent a sabbatical at Cambridge for the Newton Institute event on “Semantics”. In 1996 I moved back into industry with a software company (Harlequin), directing some 50 developers on Information Management projects and finally became overall Technical Director before leaving to re-join academia in 1999 to take the chair in Newcastle.

Much of my research focuses on formal (compositional) development methods for concurrent systems and support systems for formal reasoning. Major avenues of current research are listed below. I also retain a strong interest in the history of formal methods.

I am a Fellow of the Royal Academy of Engineering (FREng), ACM, BCS, and IET.

Thanks to Olga Petrovska for the (BCTCS) photo.

More Details

Formal methods for concurrency

Reasoning about concurrency is a major research challenge. Methods such as rely/guarantee thinking and (various) separation logics certainly help but more research is required.

More Details

Leverhulme project

I have a strong interest in -and commitment to- recording the history of our subject. this research is currently funded by a grant from the Leverhulme Trust to study and record the history of formal approaches to the development of concurrent software. The intention is to write a book on the subject and, despite Covid-19, a solid foundation already exists. In order to release our writings incrementally, we have started populating these Leverhulme project web pages.


Earlier related publications include:

Dependable Infrastructures

Planning future infrastructures.

The Infrastructure Transitions Research Consortium was an EPSRC Programme Grant looking at the way in which crucial infrastructure systems will adapt to changes such as those that might be brought about by climate and population changes. Most of the resource in ITRC was focussed on the physical infrastructures (energy, transport, water and waste). Our involvement focused on the interaction with ICT.

More Details

AI4FM

Learning proof strategies from experts.

(During and) since my time in IBM, I have had several tries at building support systems for engineers who are trying to use formal methods and I have used a number of systems developed by others (the first of which was Jim Kimg's "Effigy" system). Based on extensive industry industrial experience in the DEPLOY project, I developed the view that there was an unexplored way of using AI techniques. The AI4FM project was joint with Alan Bundy and his colleagues and explored how AI can be used to learn high-level strategies that are used by experts.

The funding for the AI4FM project has now finished but we are still working on a large Technical Report that will collect the main results.

More Details

LPF

Logic of partial functions.

Partial functions are those that can fail to denote proper values for some argument combinations (one can say such functions and/or operators are undefined for some arguments). Partiality occurs frequently in the specification of computer systems and in attempts to prove formally that designs satisfy their specifications. The "Logic of Partial Functions" is a non-classical logic that makes such reasoning both sound and convenient. I continue to do research on LPF.

More Details

Semantics Library

I have initiated an on-line library of semantics with scanned versions of many source documents that are not easy to obtain. In many cases these documents are now searchable.

VDM

Although I do not limit my interest in formal methods to VDM, I do still try to stay abreast of such research and provide pointers to source material.

More Details

RODIN & DEPLOY

The EU-funded Rodin project evolved methods and developed tool support for the Event-B method; the larger, industrial project DEPLOY was also EU funded and investigated the transfer of the methods and tools to our industrial collaborators.

Industrial Deployment of System Engineering Methods is an important summary book.

Editorial (current)