Tim Denvir

Last updated

B. Tim Denvir
Born1939
Citizenship British
Alma mater Trinity College, Cambridge
Known for Software engineering, formal methods
Awards STL Creativity Award
Scientific career
Fields Computer science
Institutions Texas Instruments, Elliott Brothers, University of London, ICL, STL, Praxis, Brunel University, City University

Tim Denvir (born 1939) is a British software engineer, specialising in formal methods. [1]

Contents

Denvir studied for a Mathematics degree at Trinity College, Cambridge during 1959–1962. [2]

Before his degree, during 1958–1959, Tim Denvir was an engineering assistant at Texas Instruments, designing, building and testing electronic circuits using discrete semiconductors. After his degree, during 1962–1965, he was a systems programmer with Elliott Brothers, programming operating systems and device drivers. During 1965–1969, he was a systems programmer at the University of London Atlas Computing Service, undertaking systems programming for the Atlas computer and compiler design. During 1969–1971, he was a project manager with RADICS, working on ALGOL 60 compilers. [3]

During 1971–1972, Denvir was a principal technical officer at International Computers Limited (ICL), working on unifying compiler design for the ICL 2900 Series of mainframe computers. During 1972–1986, he was a department manager and then from 1980 chief research engineer at the Standard Telecommunication Laboratories (STL), working on project management, technical education, and research. He won the STL Creativity Award. During 1986–1991, he was a senior/principal consultant at Praxis Systems plc, seconded for part of the time to the Information Technology Division of the UK Government Department of Trade and Industry (DTI). During 1991–2003, he was Director of Translimina Ltd. [2]

Academically, during 1988–1989, Denvir was an Associate Reader at Brunel University, teaching formal methods. During 1992–1994, he was Honorary Visiting Professor at City University in London, where he developed and delivered a course on denotational semantics. [2]

Denvir has been a member of the editorial board for the Formal Aspects of Computing journal (1989-2003) and the Springer FACIT book series. He was a member of the BSI IST/51-119 Vienna Development Method (VDM) Standardisation Committee. He was the Secretary of VDM Europe (1986–88 & 1991) and Chairman of the FACS Specialist Group (1993–1995). More recently he has been editor of the associated FACS FACTS . [4]

Tim Denvir has authored/edited/translated a number of books, including: [5]

Interests

Tim has been a keen hill-walker and "compleated" (in the parlance of the Scottish Mountaineering Club) all of the 282 Munros (the Scottish hills over 3,000 feet) in 2011, becoming Munroist number 4,855. [6]

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.

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">Peter Landin</span> British computer scientist (1930–2009)

Peter John Landin was a British computer scientist. He was one of the first to realise that the lambda calculus could be used to model a programming language, an insight that is essential to the development of both functional programming and denotational semantics.

<span class="mw-page-title-main">Jonathan Bowen</span> British computer scientist

Jonathan P. Bowen FBCS FRSA is a British computer scientist and an Emeritus Professor at London South Bank University, where he headed the Centre for Applied Formal Methods. Prof. Bowen is also the Chairman of Museophile Limited and has been a Professor of Computer Science at Birmingham City University, Visiting Professor at the Pratt Institute, University of Westminster and King's College London, and a visiting academic at University College London.

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.

<span class="mw-page-title-main">Cliff Jones (computer scientist)</span> British computer scientist (born 1944)

Clifford "Cliff" B. Jones is a British computer scientist, specializing in research into formal methods. He undertook a late DPhil at the Oxford University Computing Laboratory under Tony Hoare, awarded in 1981. Jones' thesis proposed an extension to Hoare logic for handling concurrent programs, rely/guarantee.

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

Professor Dines Bjørner is a Danish computer scientist.

The Z User Group (ZUG) was established in 1992 to promote use and development of the Z notation, a formal specification language for the description of and reasoning about computer-based systems. It was formally constituted on 14 December 1992 during the ZUM'92 Z User Meeting in London, England.

<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.

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.

Michael ("Mike") William Shields, January 20, 1950 - September 24, 2023 (aged 73) was a British computer scientist.

Peter Lucas was an Austrian computer scientist and university professor.

The Message Authenticator Algorithm (MAA) was one of the first cryptographic functions for computing a message authentication code (MAC).

<span class="mw-page-title-main">Anders P. Ravn</span> Danish computer scientist (1947–2019)

Anders Peter Ravn was a Danish computer scientist.

<span class="mw-page-title-main">Sergiy Vilkomir</span> Ukrainian-born computer scientist (1956–2020)

Sergiy A. Vilkomir was a Ukrainian-born computer scientist.

<span class="mw-page-title-main">Hussein Zedan</span>

Hussein S. M. Zedan was a computer scientist of Egyptian descent, mainly based in the United Kingdom.

<span class="mw-page-title-main">Ken Robinson (computer scientist)</span> Australian computer scientist (1938–2020)

Kenneth ("Ken") Arthur Robinson was an Australian computer scientist. He has been called "The Father of Formal Methods in Australia".

References

  1. ↑ Denvir, Tim (1 March 2017). "Fifty Years of Formal Methods in Software Engineering: Personal View". YouTube . BCS-FACS . Retrieved 28 February 2021.
  2. 1 2 3 Denvir, Tim (2020). "Curriculum Vitae" (PDF).
  3. ↑ Denvir, Tim; Astarte, Troy (3 December 2020). "Algol 60 @ 60". YouTube . BCS-FACS . Retrieved 28 February 2021.
  4. ↑ "FACS: Newsletters". BCS . Retrieved 28 February 2021.
  5. ↑ "Tim Denvir books". Amazon.co.uk . Amazon . Retrieved 28 February 2021.
  6. ↑ "Tim Denvir". Scottish Mountaineering Club . Retrieved 30 January 2024.
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.