Computing Atlas

How Computing Was Built
Sign In
Text size
100%
Theme

Switch Atlas

Field

Formal Methods

Also Known As Formal Verification
Software And Its Engineering

Formal methods are mathematically rigorous techniques for the specification, development, analysis and verification of software and hardware systems. They apply theoretical computer science foundations to improve system reliability and robustness, comparable to the mathematical analysis used in other engineering disciplines. This description is adapted from Wikipedia contributors under CC BY-SA 4.0; changes were made. https://creativecommons.org/licenses/by-sa/4.0/

Facts
Origin Year
1969 1
Tony Hoare's 1969 paper An Axiomatic Basis for Computer Programming, building on Robert Floyd's 1967 work on program semantics, is the field's conventionally cited formal starting point.
Core Concern
Mathematically specifying and, often with automated tool support, verifying that a software or hardware system meets its intended specification; gained recognition in the 1950s and 1960s through work such as John Backus's formal notation for ALGOL 58 syntax, later formalized as Backus-Naur form. 1
Connections

Associated With

Computer Algebra, Fields
John Backus, Pioneers
Source Wikipedia: Formal Methods
Programming Language Theory, Fields
Source Wikipedia: Formal Methods
Tony Hoare, Pioneers

Tony Hoare's 1969 paper An Axiomatic Basis for Computer Programming introduced Hoare logic, a foundational formal system for reasoning about program correctness, already cited on this field's own origin-year fact.

Source Wikipedia: Tony Hoare

Includes

Amir Pnueli, Pioneers
Source Wikipedia: Amir Pnueli
Anders P. Ravn, Pioneers
Source Wikipedia: Anders P. Ravn
Christine Paulin-Mohring, Pioneers
Source Christine Paulin-Mohring (Wikipedia)
Coq (proof assistant), Programming Languages
Source Rocq - Wikipedia
David Harel, Pioneers
Source David Harel (Wikipedia)
David L. Dill, Pioneers
Source David L. Dill (Wikipedia)
David Luckham, Pioneers
Source David Luckham, Wikipedia
Davis-Putnam algorithm, Algorithms
Source Davis-Putnam algorithm (Wikipedia)
Dines Bjorner, Pioneers
Source Dines Bjorner, Wikipedia
E. Allen Emerson, Pioneers
Source Wikipedia: E. Allen Emerson
Edmund M. Clarke, Pioneers
Source Wikipedia: Edmund M. Clarke
Eric Hehner, Pioneers
Source Wikipedia: Eric Hehner
George Necula, Pioneers
Source George Necula (Wikipedia)
Gerard J. Holzmann, Pioneers
Source Gerard J. Holzmann (Wikipedia)
Greg Nelson (computer scientist), Pioneers
Source Greg Nelson (computer scientist) (Wikipedia)
Hans Langmaack, Pioneers
Source Hans Langmaack (Wikipedia)
He Jifeng, Pioneers
Source Wikipedia: He Jifeng
Hussein Zedan, Pioneers
Source Hussein Zedan (Wikipedia)
Insup Lee, Pioneers
Source Insup Lee (Wikipedia)
J Strother Moore, Pioneers
Source J Strother Moore (Wikipedia)
Jayadev Misra, Pioneers
Source Jayadev Misra (Wikipedia)
Jonathan Bowen, Pioneers
Source Wikipedia: Jonathan Bowen
Joseph Goguen, Pioneers
Source Wikipedia: Joseph Goguen
Joseph Sifakis, Pioneers
Source Wikipedia: Joseph Sifakis
Kim Guldstrand Larsen, Pioneers
Source Kim Guldstrand Larsen (Wikipedia)
Lawrence Paulson, Pioneers
Source Wikipedia: Lawrence Paulson
Marta Kwiatkowska, Pioneers
Source Marta Kwiatkowska (Wikipedia)
Mathai Joseph, Pioneers
Source Mathai Joseph - Wikipedia
Matt Kaufmann, Pioneers
Source Matt Kaufmann (Wikipedia)
Michael Backes, Pioneers
Source Michael Backes, Wikipedia
Paritosh Pandya, Pioneers
Source Paritosh Pandya (Wikipedia)
Patrick Cousot, Pioneers
Source Wikipedia: Patrick Cousot
Peter O'Hearn, Pioneers
Source Wikipedia: Peter O'Hearn
Radhia Cousot, Pioneers
Source Radhia Cousot (Wikipedia)
Rajeev Alur, Pioneers
Source Rajeev Alur, Wikipedia
Randal Bryant, Pioneers
Source Randal Bryant, Wikipedia
Robert France, Pioneers
Source Wikipedia: Robert France
Robert K. Brayton, Pioneers
Source Robert K. Brayton, Wikipedia
Robert L. Constable, Pioneers
Source Wikipedia: Robert L. Constable
Robin Milner, Pioneers
Source Wikipedia: Robin Milner
Sandrine Blazy, Pioneers
Source Sandrine Blazy (Wikipedia)
Sergiy Vilkomir, Pioneers
Source Wikipedia: Sergiy Vilkomir
Tobias Nipkow, Pioneers
Source Tobias Nipkow, Wikipedia
Zhou Chaochen, Pioneers
Source Wikipedia: Zhou Chaochen
Sources
1. Wikipedia: Formal Methods
Wikimedia Foundation
  • Verification section
    Formal verification is the use of software tools to prove properties of a formal specification, or to prove that a formal model of a system implementation satisfies its specification.
  • History section
    In the ALGOL 58 report, John Backus presented a formal notation for describing programming language syntax, later named Backus normal form then renamed Backus-Naur form (BNF).
  • Introduction
    In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems.
  • Associated With: Programming Language Theory, Fundamentals section
    Formal methods employ a variety of theoretical computer science fundamentals, including logic calculi, formal languages, automata theory, control theory, program semantics, type systems, and type theory.
  • Associated With: John Backus, Specification section
    In the ALGOL 58 report, John Backus presented a formal notation for describing programming language syntax, later named Backus normal form then renamed Backus-Naur form (BNF).
  • In Group: Software Development, Architecture and Verification, lead section
View the Source
Wikipedia: Tony Hoare
Wikimedia FoundationAssociated With: Tony HoareView the Source
Wikipedia: Robin Milner
Wikimedia FoundationIncludes: Robin Milner, Contributions
Quote, Includes: Robin Milner, Contributions
He developed Logic for Computable Functions (LCF), one of the first tools for automated theorem proving.
View the Source
Michael Backes, Wikipedia
Includes: Michael Backes, Lead section
Quote, Includes: Michael Backes, Lead section
formal methods, cryptography and privacy-enhancing technologies
View the Source
Insup Lee (Wikipedia)
Includes: Insup Lee, Lead section
Quote, Includes: Insup Lee, Lead section
formal methods and tools
View the Source
Paritosh Pandya (Wikipedia)
Includes: Paritosh Pandya, Lead
Quote, Includes: Paritosh Pandya, Lead
Pandya's main research interest is in the area of formal methods, including real-time systems.
View the Source
Gerard J. Holzmann (Wikipedia)
Includes: Gerard J. Holzmann, Infobox: fields
Quote, Includes: Gerard J. Holzmann, Infobox: fields
Model Checking
View the Source
Radhia Cousot (Wikipedia)
Includes: Radhia Cousot, Lead
Quote, Includes: Radhia Cousot, Lead
Radhia Cousot, née Rezig (6 August 1947-1 May 2014) was a French computer scientist known for inventing abstract interpretation.
View the Source
Christine Paulin-Mohring (Wikipedia)
Includes: Christine Paulin-Mohring, Lead
Quote, Includes: Christine Paulin-Mohring, Lead
Christine Paulin-Mohring (born 1962) is a mathematical logician and computer scientist, and Professor at the Faculté des Sciences of Paris-Saclay University, best known for developing the interactive theorem prover Rocq.
View the Source
Davis-Putnam algorithm (Wikipedia)
Includes: Davis-Putnam algorithm, Lead [in-field]
Quote, Includes: Davis-Putnam algorithm, Lead [in-field]
using a resolution-based decision procedure for propositional logic
View the Source
Wikipedia: Joseph Sifakis
Wikimedia FoundationIncludes: Joseph Sifakis, Lead paragraphView the Source
Wikipedia: Amir Pnueli
Wikimedia FoundationIncludes: Amir Pnueli, Lead paragraphView the Source
Wikipedia: Edmund M. Clarke
Wikimedia FoundationIncludes: Edmund M. Clarke, Lead paragraphView the Source
Wikipedia: E. Allen Emerson
Wikimedia FoundationIncludes: E. Allen Emerson, Lead paragraphView the Source
Wikipedia: Jonathan Bowen
Wikimedia FoundationIncludes: Jonathan Bowen, Lead paragraphView the Source
Wikipedia: Lawrence Paulson
Wikimedia FoundationIncludes: Lawrence Paulson, Lead paragraphView the Source
Rajeev Alur, Wikipedia
Includes: Rajeev Alur, Lead paragraphView the Source
Randal Bryant, Wikipedia
Includes: Randal Bryant, Lead paragraphView the Source
David L. Dill (Wikipedia)
Includes: David L. Dill, Lead paragraphView the Source
Sandrine Blazy (Wikipedia)
Includes: Sandrine Blazy, Lead paragraphView the Source
Rocq - Wikipedia
Includes: Coq (proof assistant), Lead paragraphView the Source
Wikipedia: Zhou Chaochen
Wikimedia FoundationIncludes: Zhou Chaochen, Infobox field and known_for, lead paragraphView the Source
Wikipedia: Joseph Goguen
Wikimedia FoundationIncludes: Joseph Goguen, Infobox field and known_for, lead paragraphView the Source
Wikipedia: Patrick Cousot
Wikimedia FoundationIncludes: Patrick Cousot, Infobox field and known_for, lead paragraphView the Source
Wikipedia: He Jifeng
Includes: He Jifeng, Infobox field and known_for, lead paragraphView the Source
Wikipedia: Eric Hehner
Includes: Eric Hehner, Infobox field and known_for, lead paragraphView the Source
Tobias Nipkow, Wikipedia
Includes: Tobias Nipkow, Infobox field and known_for, lead paragraphView the Source
Mathai Joseph - Wikipedia
Includes: Mathai Joseph, Infobox field and known_for, lead paragraphView the Source
Wikipedia: Robert L. Constable
Includes: Robert L. Constable, Infobox field and known_for, lead paragraphView the Source
Wikipedia: Robert France
Includes: Robert France, Infobox field and known_for, lead paragraphView the Source
Wikipedia: Sergiy Vilkomir
Includes: Sergiy Vilkomir, Infobox field and known_for, lead paragraphView the Source
Wikipedia: Anders P. Ravn
Wikimedia FoundationIncludes: Anders P. Ravn, Infobox field and known_for, lead paragraphView the Source
Hussein Zedan (Wikipedia)
Includes: Hussein Zedan, Infobox field and known_for, lead paragraphView the Source
Hans Langmaack (Wikipedia)
Includes: Hans Langmaack, Infobox field and known_for, lead paragraphView the Source
Greg Nelson (computer scientist) (Wikipedia)
Includes: Greg Nelson (computer scientist), Infobox field and known_for, lead paragraphView the Source
George Necula (Wikipedia)
Includes: George Necula, Infobox field and known_for, lead paragraphView the Source
David Harel (Wikipedia)
Includes: David Harel, Infobox field and known_for, lead paragraphView the Source
Matt Kaufmann (Wikipedia)
Includes: Matt Kaufmann, Infobox field and known_for, lead paragraphView the Source
J Strother Moore (Wikipedia)
Includes: J Strother Moore, Infobox field and known_for, lead paragraphView the Source
Jayadev Misra (Wikipedia)
Includes: Jayadev Misra, Infobox field and known_for, lead paragraphView the Source
Wikipedia: Peter O'Hearn
Wikimedia FoundationIncludes: Peter O'Hearn, Infobox: fields
Quote, Includes: Peter O'Hearn, Infobox: fields
Programming languages Program analysis Formal verification Theoretical computer science
View the Source
David Luckham, Wikipedia
Includes: David Luckham, Infobox: known_for
Quote, Includes: David Luckham, Infobox: known_for
Lisp Automated theorem proving Stanford Pascal Verifier Complex event processing Rational Software
View the Source
Dines Bjorner, Wikipedia
Includes: Dines Bjorner, Lead
Quote, Includes: Dines Bjorner, Lead
He specializes in research into domain engineering, requirements engineering and formal methods.
View the Source
Robert K. Brayton, Wikipedia
Includes: Robert K. Brayton, Infobox: known_for
Quote, Includes: Robert K. Brayton, Infobox: known_for
Logic synthesis, formal verification, circuit simulation
View the Source
Marta Kwiatkowska (Wikipedia)
Includes: Marta Kwiatkowska, Infobox: fields
Quote, Includes: Marta Kwiatkowska, Infobox: fields
Computer Science Automated verification Model checking, Probabilistic quantitative model checking Safety and robustness verification of deep learning
View the Source
Kim Guldstrand Larsen (Wikipedia)
Includes: Kim Guldstrand Larsen, Lead
Quote, Includes: Kim Guldstrand Larsen, Lead
His field of research includes modeling, validation and verification, performance analysis, and synthesing of real-time, embedded, and cyber-physical systems utilizing and contributing to concurrency theory and model checking.
View the Source
Comments (0)
No comments yet. Be the first to share a thought.
Reader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.