Prof. Cliff Jones of Newcastle University (UK) has been awarded the first FME Fellowship. The Fellowships are awarded every three years in recognition of technical breakthroughs and pioneering work in advancing, applying, and promoting mathematically rigorous methods for the design of computing systems.
The first call for nominations was issued in January 2015, and on 25 June 2015 this process was concluded. In a ceremony at the 20th International Symposium on Formal Methods (FM 2015) Prof. Jones was announced as being the first Fellow of Formal Methods Europe. After Prof. Ana Cavalcanti, the Chair of FME, introduced the new FME Fellow and explained the selection process, Prof. Cliff Jones shared his insights in a talk with the title “Intuition before Formalism” about his work and scientific achievements (slides and references). At the end of the ceremony, Prof. Jones was presented with a certificate and medal.
The FME Awards Committee motivated its decision as follows:
Cliff Jones is one of the world’s most distinguished computer scientists, with an outstanding international reputation for his research and leadership in the discipline, where he has a unique record of major contributions to academia, to industry, to policy, and of service.
He has consistently emphasised the crucial role of formalism in the design process. He worked with others during the 1970s at IBM, devising the Vienna Development Method (VDM), where rigorous program development is based on data refinement (reification). This pioneering work has been used in industry and has led to the development of a wide class of languages of both practical and theoretical importance; this includes ASM, B, Z, the refinement calculus, and RAISE. Among several books, his two texts on using VDM in program design have over 4,000 Google Scholar references.
Jones pioneered the use of rely-guarantee conditions in reasoning about shared-variable concurrency, and has led it for 35 years. While the work on rely-guarantee started off in a VDM-like notation, its underpinning concepts are more fundamental; the legacy is rely-guarantee thinking, with much wider influence. For example, Separation Logic, recognised as one of the most important theoretical developments of recent years, uses rely-guarantee thinking as a key concept to ensure scalability. Jones has also made fundamental contributions to the use of logic in program development by developing the Logic of Partial Functions, which directly supports reasoning about undefined expressions.
He was also among the first to push forward the practical use of formal methods. His research in a variety of pilot collaborative projects in the early days led to corporate investments in formal methods for software and hardware by companies including ARM, IBM, Intel, Microsoft, and QinetiQ.
Jones founded in 1989 a major international journal in the field of formal methods, Formal Aspects of Computing, and a leading international conference, the Formal Methods Symposium. He has been influential in IFIP, as a long-standing member and chair of WG 2.3 on Programming Methodology, and as a founding member of WG 1.9/2.15 on Verified Software. His policy work, for example for the UK Royal Academy of Engineering, has done much to engage public debate on the dependability of computing systems. He has helped guide and mentor the careers of numerous young computer scientists.
This far-sighted commitment to the development of formal methods has helped shape our community. We are fortunate to be able to show our gratitude by awarding a Formal Methods Europe Fellowship to Cliff Jones.
