- Andrius Velykis has joined the "Taming Concurrency" project.
- The "Taming Concurrency" project has started - Nisansala Yatapanage started as a post-Doc researcher on September 15th (see more under Concurrency Research).
- An AI4FM paper "Ours is to reason why" has been published.
- A paper "Revising Basic Theorem Proving Algorithms to Cope with the Logic of Partial Functions" on the mechanisation of the Logic of Partial Functions has been published.
- Preparations for FM 2014 in Singapore are well advanced.
- Cliff is also on the PC of ICTAC 2014.
- SETTA aims to promote strong connections between Chinese an non-Chinese computer scientists - the first conference (of which Cliff is General Chair) will be in Nanjing in August 2014.
I'm a Professor of Computing Science at Newcastle University with research interests ranging from theoretical computer science to dependability applications. Now back in academia, I've spent over 20 years of my research 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 to supervise my doctorate solely on the basis of my publications. 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 small 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.
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 am a Fellow of the Royal Academy of Engineering (FREng), ACM, BCS, and IET.
Reasoning about concurrent systems using rely/guarantee and separation logic.
If you think that you can build non-trivial sequential programs that satisfy their specification (have no "bugs") without formal methods, you are probably kidding yourself; but, if you are honest, you have have to confess that there is no chance with concurrent programs. Reasoning about concurrency is a major research challenge. Methods such as rely/guarantee thinking and (various) separation logics certainly help - but there is much more research required. We have an exciting pair of projects: (UK) EPSRC are funding "Taming Concurrency" which will employ two post-Docs and the Australian Research Council is funding a project led by Ian Hayes with the title "Understanding concurrent programmes using rely-guarantee thinking".
- (Recent) Cliff B. Jones, Balancing Expressiveness in Formal Approaches to Concurrency, 2013 (submitted to Formal Aspects of Computing).
- Cliff B. Jones, Tentative steps toward a development method for interfering programs, 1983.
Learning proof strategies from the expert.
Going back to 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. 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 is joint with Alan Bundy and his colleagues and is exploring how AI can be used to learn high-level strategies that are used by experts.
Planning future infrastructures.
The "Infrastructure Transitions Research Consortium" is 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 is focussed on the physical infrastructures (energy, transport, water and waste). Our involvement focuses on the interaction with ICT.
- Roberta Velykiene and Cliff B. Jones, A Fast Track Analysis of ICT Constraints on Evolving Physical Infrastructure, 2011.
- A Fast Track Analysis of strategies for infrastructure provision in Great Britain: Technical report, 2012.
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.
- Cliff B. Jones, Matthew J. Lovert, L. Jason Steggles, Revising Basic Theorem Proving Algorithms to Cope with the Logic of Partial Functions, 2013.
History of formal methods
History of formal methods (including collaboration with Peter Mosses' PLanCompS project). This includes making source material available on-line.
Although I do not limit my interest in formal methods to the earlier work on VDM, I do still try to stay abreast of such research and provide pointers to source material.
RODIN & DEPLOY
The EU-funded Rodin project enveloped methods and 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.
Although I now spend most of my time doing research, I happen to love teaching. Apart from the occasional "guest" lecture on other courses, my main commitment at the moment is to CSC3321: Understanding Programming Languages.