Recent news
- Ana Cavalcanti and James Baxter did me the honour of editing a Festschrift (Part 1, Part 2); incredibly none of the authors disclosed what was going on before Ana presented the volumes to me at a dinner in York!
- A joint paper with colleagues at University of Queensland on recent Rely-Guarantee research has been published in LNCS; a further draft paper is on arXiv.
- The productive collaboration with Alan Burns at York on applying Rely-Guarantee thinking to Real-Time Systems continues: we had a joint open-access paper published in FMiCS which was also selected as a Journal First talk at FM-24; another joint paper has appeared in the Festschrift for Jim Woodcock.
- I was funded by the Leverhulme Trust to study and record the history of formal approaches to the development of concurrent software. The project (RPG-2019-020) finished in 2023. Troy Astarte was a post-Doc; we each spoke at the HaPoC conference in 2021 and papers have appeared (2023) in Minds and Machines (Troy, Cliff); a further by-product of this work is a paper on the trail from early research on concurrency by Ashcroft and Manna (via (Owicki) to the rely-guarantee ideas.
- Work with NIsansala Yatapanage at ANU on using Rely-Guarantee ideas to specify security protocols gave rise to a paper at the 2024 Overture Workshop in Milan; pending publication of the conference proceedings, a draft is accessible on arXiv.
- "Theories of programming: the life and works of Tony Hoare" has been published by ACM (co-edited with Jayadev Misra).
- "Understanding Programming Languages" has been published by Springer.
A set of slides that could form the basis of a course is available as a Zip file ---
(please read the information at the beginning of root.tex)
the slides are licensed under a Creative Commons Attribution-ShareAlike 4.0 International License
- I have 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.
About me
My research interests are mainly in “formal methods“. Nominal "retirement" changed little in my life: I continue to work as an Emeritus Professor of Computing Science at Newcastle University..
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 (FREngi 2003), ACM (FACM in 1995), BCS, and IET; in 2015 I was the first person to be made a Fellow of Formal Methods Europe.
Thanks to Olga Petrovska for the (BCTCS) photo.
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.
- Concurrency: a joint paper with Nisansala Yatapanage on the limits of Rely/Guarantee relations has been accepted by Formal Aspects of Computing - 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 available; and A Guide to Rely/Guarantee Thinking has now been published.
- (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.
Leverhulme Trust (project RPG-2019-020)
Separation and interference: learning from the history of concurrency
Cliff Jones had a Leverhulme grant to study and document the history of research on formal methods for concurrency. The 3.5 year project has now finished but publications by Jones and Astarte. continue to appear:
- Astarte and Jones both spoke at the 2021 HaPoC event and have had journal (Minds and Machines) papers published in the post-conference proceedings (Troy, Cliff).
- "Theories of programming: the life and works of Tony Hoare" (co-edited with Jayadev Misra) has been published by ACM.
- A FAC journal paper (joint with Martyn Thomas) focusses on the deployment of formal methods results.
- A ECRTS paper (joint with Alan Burns).
- My 2022 BCTCS talk: video available
- A paper (presented at CiE-17 in Turku) is Turing's 1949 paper in Context.
- The proceedings of the Paris HaPoP are available and a longer Technical Report version compares four formal semantic descriptions of ALGOL 60.
- A paper that looks at the "challenges" represented in formal semantic descriptions (was the basis of my HaPoC talk in Brno and) has also been been published (again a Technical Report is available).
- A much earlier paper about formal methods for verification is (Jones, 2003).
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.
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.
- Tool Support (for formal methods)
- A Schloss Dagstuhl event that we organised on related topics
- a (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.
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.
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.
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)
- Founding Editor of Formal Aspects of Computing and editor-in-chief from 1989-2009 (Jim Woodcock is now editor-in-chief)
- A foundation editor of Journal of Universal Computer Science
- Advisor to the Journal of Logic and Computation