Cliff Jones (computer scientist)

Last updated

Cliff Jones
Cliff Jones Swansea.png
Cliff Jones in Swansea
Born (1944-06-01) 1 June 1944 (age 79)
Nationality British
Alma mater University of Oxford
Known for Vienna Development Method
Scientific career
Institutions IBM Laboratory Vienna
Victoria University of Manchester
Newcastle University
Thesis Development Methods for Computer Programs Including a Notion of Interference
Doctoral advisor C. A. R. Hoare [1]
Doctoral students John Fitzgerald
Tobias Nipkow

Clifford "Cliff" B. Jones FREng [2] (born 1 June 1944) is a British computer scientist, specializing in research into formal methods. [3] He undertook a late DPhil at the Oxford University Computing Laboratory (now the Oxford University Department of Computer Science) under Tony Hoare, awarded in 1981. Jones' thesis proposed an extension to Hoare logic for handling concurrent programs, rely/guarantee. [4]

Contents

Prior to his DPhil, Jones worked for IBM, between the Hursley and Vienna Laboratories. In Vienna, Jones worked with Peter Lucas, Dines Bjørner and others on the Vienna Development Method (VDM), originally as a method for specifying the formal semantics of programming languages, and subsequently for specifying and verifying programs. [5]

Cliff Jones was a professor at the Victoria University of Manchester in the 1980s and early 1990s, worked in industry at Harlequin for a period, and is now a Professor of Computing Science at Newcastle University. He has been editor-in-chief of the Formal Aspects of Computing journal. [6]

As well as formal methods, Jones also has interests in interdisciplinary aspects of computer science and the history of computer science. [7] [8]

Books

Jones has authored and edited many books, including:

Related Research Articles

<span class="mw-page-title-main">Z notation</span> Formal specification language used for describing and modelling computing systems

The Z notation is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.

<span class="mw-page-title-main">Tony Hoare</span> British computer scientist

Sir Charles Antony Richard Hoarehor is a British computer scientist who has made foundational contributions to programming languages, algorithms, operating systems, formal verification, and concurrent computing. His work earned him the Turing Award, usually regarded as the highest distinction in computer science, in 1980.

The Vienna Development Method (VDM) is one of the longest-established formal methods for the development of computer-based systems. Originating in work done at the IBM Laboratory Vienna in the 1970s, it has grown to include a group of techniques and tools based on a formal specification language—the VDM Specification Language (VDM-SL). It has an extended form, VDM++, which supports the modeling of object-oriented and concurrent systems. Support for VDM includes commercial and academic tools for analyzing models, including support for testing and proving properties of models and generating program code from validated VDM models. There is a history of industrial usage of VDM and its tools and a growing body of research in the formalism has led to notable contributions to the engineering of critical systems, compilers, concurrent systems and in logic for computer science.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

<span class="mw-page-title-main">Per Brinch Hansen</span> Danish-American computer scientist

Per Brinch Hansen was a Danish-American computer scientist known for his work in operating systems, concurrent programming and parallel and distributed computing.

The B method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software.

Jean-Raymond Abrial is a French computer scientist and inventor of the Z and B formal methods.

<span class="mw-page-title-main">Dines Bjørner</span> Danish computer scientist

Professor Dines Bjørner is a Danish computer scientist.

Zhou Chaochen is a Chinese computer scientist.

<span class="mw-page-title-main">BCS-FACS</span> Specialist Group of the BCS

BCS-FACS is the BCS Formal Aspects of Computing Science Specialist Group.

John S. Fitzgerald FBCS is a British computer scientist. He is a professor at Newcastle University. He was the head of the School of Computing before taking on the role of Dean of Strategic Projects in the university’s Faculty of Science, Agriculture and Engineering. His research interests are in the area of dependable computer systems and formal methods, with a background in the VDM. He is a former Chair of Formal Methods Europe and committee member of BCS-FACS.

<span class="mw-page-title-main">He Jifeng</span> Chinese computer scientist

He Jifeng is a Chinese computer scientist.

Prentice Hall International Series in Computer Science was a series of books on computer science published by Prentice Hall.

<span class="mw-page-title-main">Heinz Zemanek</span> Austrian computer pioneer

Heinz Zemanek was an Austrian computer pioneer who led the development, from 1954 to 1958, of one of the first complete transistorised computers on the European continent. The computer was nicknamed Mailüfterl — Viennese for "May breeze" — in reference to Whirlwind, a computer developed at MIT between 1945 and 1951.

The Meta-IV was an early version of the specification language of the Vienna Development Method formal method for the development of computer-based systems.

Model-based specification is an approach to formal specification where the system specification is expressed as a system state model. This state model is constructed using well-understood mathematical entities such as sets and functions. System operations are specified by defining how they affect the state of the system model.

<span class="mw-page-title-main">Dansk Datamatik Center</span> Danish software research and development centre

Dansk Datamatik Center (DDC) was a Danish software research and development centre that existed from 1979 to 1989. Its main purpose was to demonstrate the value of using modern techniques, especially those involving formal methods, in software design and development.

IBM Laboratory Vienna was an IBM research laboratory based in Vienna, Austria.

Peter Lucas was an Austrian computer scientist and university professor.

Tim Denvir is a British software engineer, specialising in formal methods.

References

  1. ↑ Cliff Jones at the Mathematics Genealogy Project
  2. ↑ "List of Fellows". Royal Academy of Engineering . Archived from the original on 9 August 2014.
  3. ↑ "Bio · Cliff B Jones". UK: Newcastle University. Archived from the original on 23 June 2015. Retrieved 18 December 2020.
  4. ↑ Jones, C.B. (June 1981). Development Methods for Computer Programs including a Notion of Interference (PDF) (DPhil thesis). Oxford University.
  5. ↑ "Research · Cliff B Jones". UK: Newcastle University. Archived from the original on 13 July 2014. Retrieved 18 December 2020.
  6. ↑ Formal Aspects of Computing. Vol. 1. Association for Computing Machinery. 1989. Retrieved 19 August 2018.
  7. ↑ Cliff B. Jones at DBLP Bibliography Server OOjs UI icon edit-ltr-progressive.svg
  8. ↑ Cliff B. Jones: Publication List Archived 12 March 2012 at the Wayback Machine , Scientific Commons.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.