- Concurrency: a joint paper with Nisansala Yatapanage on the limits of Rely/Guarantee relations has been submitted to a journal - a draft is available as a Technical Report.
- Two related papers on Concurrency project are: Reasoning about Separation Using Abstraction and Reification and Possible values: Exploring a concept for concurrency
- These follow on from the root-and-branch revision of Rely/Guarantee Thinking (see Balancing Expressiveness in Formal Approaches to Concurrency and Laws and semantics for rely-guarantee refinement)
- Ian Hayes gave a Tutorial on Rely/Guarantee research at SETSS-2017 the slides are here; the proceedings are in press.
- Work on the history of formal methods has stepped up since Troy Astarte started his PhD on the History of Language Semantics. Troy presented our joint paper at HaPoP in Paris; the proceedings are now "in press" and a long Technical Report version compares four formal semantic descriptions of ALGOL 60.
- A related paper that looks at the "challenges" represented in formal semantic descriptions (was the basis of my HaPoC talk in Brno in October 2017 and) is also "in press" - again a Technical Report is available.
Warning: I'm rearranging the PDFs (in particular adding a lot of TRs) - until I'm finished there might be some incorrect pointers - in fact, I'm moving to using DoIs which are more stable than URLs
I'm a Professor of Computing Science at Newcastle University with research interests mainly in “formal methods“.
I've actually 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.
Designing concurrent systems.
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 more research is required. We had an exciting pair of projects: (UK) EPSRC funded Taming Concurrency on which Nisansala Yatpanage and Andrius Velykis were the post-Docs and the Australian Research Council funded a project with the title Understanding concurrent programmes using rely-guarantee thinking led by Ian Hayes.
- (Recent) Jones, Hayes and Colvin Balancing Expressiveness in Formal Approaches to Concurrency, 2015 (available Open Source from Formal Aspects of Computing).
- (A useful summary of the original concept) Cliff B. Jones, Accommodating Interference in the Formal Design of Concurrent Object-Based Programs, 1996.
- (One source reference) Cliff B. Jones, Tentative steps toward a development method for interfering programs, 1983.
History of formal methods
I have a strong interest in, and commitment to, recording the history of our subject. The fact that Troy Astarte is working on a Historical analysis of programming language descriptions for his PhD and this has given a new impetus to the effort.
- A joint paper was accepted which Troy presented at HaPoP in Paris.
- A long Technical Report compares four formal semantic descriptions of ALGOL 60.
- An earlier paper about formal methods for verification is (Jones, 2003).
- During 2014, I collaborated with Peter Mosses' PLanCompS project.
- A paper that I wrote for a book but decided to make available as a Technical Report is Turing and Software Verification.
- We are building an on-line library of semantics with scanned versions of many source documents that are not easy to obtain.
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.
- Assessing the Long-Term Performance of Cross-Sectoral Strategies for National Infrastructure, 2014.
- National infrastructure assessment: Analysis of options for infrastructure provision in Great Britain, 2014.
Our involement ...
We now have a project (joint with EEE) that is funded by HubNet.
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.
- Tool Support (for formal methods)
- A Schloss Dagstuhl event that we organised on related topics
- recent (VSTTE) paper
- Also: mural - an earlier project that created a theorem proving assistant.
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.
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.
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.
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.
There are a variety of other things on which I spend time: