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
Formal Methods
Filter Results2 entries

Insup Lee

Formal Methods

Jayadev Misra

Formal Methods
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
Bernard Carré, Pioneers
Source SPARK (programming language) (Wikipedia)
Carolyn Talcott, Pioneers
Source Carolyn Talcott (Wikipedia)
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)
Jeannette Wing, Pioneers
Source Jeannette Wing (Wikipedia)
Jonathan Bowen, Pioneers
Source Wikipedia: Jonathan Bowen
Joseph Goguen, Pioneers
Source Wikipedia: Joseph Goguen
Joseph Sifakis, Pioneers
Source Wikipedia: Joseph Sifakis
Kaisa Sere, Pioneers
Source Kaisa Sere (Wikipedia)
Kim Guldstrand Larsen, Pioneers
Source Kim Guldstrand Larsen (Wikipedia)
Lawrence Paulson, Pioneers
Source Wikipedia: Lawrence Paulson
Leonardo de Moura, Pioneers
Source Leonardo de Moura (Wikipedia)
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
Mizar system, Programming Languages
Source Mizar system (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
Susan Gerhart, Pioneers
Source Susan Gerhart (Wikipedia)
Tobias Nipkow, Pioneers
Source Tobias Nipkow, Wikipedia

Showing 1 to 50 of 52 in Includes, page 1 of 2.

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
Leonardo de Moura (Wikipedia)
Includes: Leonardo de Moura, Lead paragraph
Quote, Includes: Leonardo de Moura, Lead paragraph
Leonardo de Moura is a Brazilian computer scientist, creator of the Lean proof assistant and co-creator of the Z3 Theorem Prover during his time at Microsoft Research.
View the Source
Carolyn Talcott (Wikipedia)
Includes: Carolyn Talcott, Lead sentence [in-group]
Quote, Includes: Carolyn Talcott, Lead sentence [in-group]
known for work in formal reasoning, especially as it relates to computers, cryptanalysis and systems biology
View the Source
Jeannette Wing (Wikipedia)
Includes: Jeannette Wing, Career and research
Quote, Includes: Jeannette Wing, Career and research
Wing has been a leading member of the formal methods community, especially in the area of Larch.
View the Source
Ursula Martin (Wikipedia)
Includes: Ursula Martin, Lead
Quote, Includes: Ursula Martin, Lead
with research interests in theoretical computer science and formal methods
View the Source
Kaisa Sere (Wikipedia)
Includes: Kaisa Sere, Biography, formal methods research
Quote, Includes: Kaisa Sere, Biography, formal methods research
She undertook formal methods research in action systems, distributed systems, hardware design, neural networks, and program refinement.
View the Source
Susan Gerhart (Wikipedia)
Includes: Susan Gerhart, Education, thesis
Quote, Includes: Susan Gerhart, Education, thesis
She completed her thesis "Verification of APL Programs" in 1972
View the Source
SPARK (programming language) (Wikipedia)
Includes: Bernard Carré, Lead, verification
Quote, Includes: Bernard Carré, Lead, verification
The SPARK language consists of a well-defined subset of the Ada language that uses contracts to describe the specification of components in a form that is suitable for both static and dynamic verification.
View the Source
Mizar system (Wikipedia)
Includes: Mizar system, Lead
Quote, Includes: Mizar system, Lead
a proof assistant, which is able to mechanically check proofs written in this language
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.

Computing Atlas

How Computing Was Built
Sign In
Text size
100%
Theme

Switch Atlas