Formal verification

program verificationverificationautomated verificationverifiedcomputer aided verificationformally correctformally verifiedprogram verifiersoftware verificationverifiability
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.wikipedia
230 Related Articles

Formal methods

formal methodformalformal analysis
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Subareas of formal verification include deductive verification (see above), abstract interpretation, automated theorem proving, type systems, and lightweight formal methods.
In computer science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically based techniques for the specification, development and verification of software and hardware systems.

Formal specification

specificationsoftware specificationspecifications
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.
Given such a specification, it is possible to use formal verification techniques to demonstrate that a system design is correct with respect to its specification.

Correctness (computer science)

correctnessprogram correctnesscorrect
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.
A termination proof is a type of mathematical proof that plays a critical role in formal verification because total correctness of an algorithm depends on termination.

Operational semantics

operationalnatural semanticsOperationally
Examples of mathematical objects often used to model systems are: finite state machines, labelled transition systems, Petri nets, vector addition systems, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as operational semantics, denotational semantics, axiomatic semantics and Hoare logic.
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms (denotational semantics).

Cryptographic protocol

protocolsecurity protocolprotocols
Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.
Cryptographic protocols can sometimes be verified formally on an abstract level.

Computation tree logic

CTLcomputational tree logicACTL
The properties to be verified are often described in temporal logics, such as linear temporal logic (LTL), Property Specification Language (PSL), SystemVerilog Assertions (SVA), or computational tree logic (CTL).
It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers which determine if a given artifact possesses safety or liveness properties.

Temporal logic

temporaltense logicsituations
The properties to be verified are often described in temporal logics, such as linear temporal logic (LTL), Property Specification Language (PSL), SystemVerilog Assertions (SVA), or computational tree logic (CTL).
Temporal logic has found an important application in formal verification, where it is used to state requirements of hardware or software systems.

Linear temporal logic

LTLlinear temporalLinear Temporal Logic (LTL)
The properties to be verified are often described in temporal logics, such as linear temporal logic (LTL), Property Specification Language (PSL), SystemVerilog Assertions (SVA), or computational tree logic (CTL).
LTL was first proposed for the formal verification of computer programs by Amir Pnueli in 1977.

Property Specification Language

PSL
The properties to be verified are often described in temporal logics, such as linear temporal logic (LTL), Property Specification Language (PSL), SystemVerilog Assertions (SVA), or computational tree logic (CTL).
It is widely used in the hardware design and verification industry, where formal verification tools (such as model checking) and/or logic simulation tools are used to prove or refute that a given PSL formula holds on a given design.

Program derivation

deriving programs
Another complementary approach is program derivation, in which efficient code is produced from functional specifications by a series of correctness-preserving steps.

Combinational logic

combinationalcombinatorial logiccombinational circuit
Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Digital electronics

digital circuitdigitaldigital technology
Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Termination analysis

terminationtermination proofensuring its termination
Techniques can also be decidable, meaning that their algorithmic implementations are guaranteed to terminate with an answer, or undecidable, meaning that they may never terminate.
A termination proof is a type of mathematical proof that plays a critical role in formal verification because total correctness of an algorithm depends on termination.

Type system

dynamicstatictype checking
Subareas of formal verification include deductive verification (see above), abstract interpretation, automated theorem proving, type systems, and lightweight formal methods.
Static type checking can be considered a limited form of program verification (see type safety), and in a type-safe language, can be considered also an optimization.

Program synthesis

generatesoftware synthesissynthesis
Program repair combines techniques from formal verification and program synthesis.
In contrast to program verification, the program is to be constructed rather than given; however, both fields make use of formal proof techniques, and both comprise approaches of different degrees of automatization.

Automated theorem proving

automated theorem provertheorem provertheorem proving
Subareas of formal verification include deductive verification (see above), abstract interpretation, automated theorem proving, type systems, and lightweight formal methods.
One of the first fruitful areas was that of program verification whereby first-order theorem provers were applied to the problem of verifying the correctness of computer programs in languages such as Pascal, Ada, Java etc. Notable among early program verification systems was the Stanford Pascal Verifier developed by David Luckham at Stanford University.

Hoare logic

Hoare tripleFloyd–Hoare logicHoare style
Examples of mathematical objects often used to model systems are: finite state machines, labelled transition systems, Petri nets, vector addition systems, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as operational semantics, denotational semantics, axiomatic semantics and Hoare logic.

Denotational semantics

denotationalfully abstractHistory of denotational semantics
Examples of mathematical objects often used to model systems are: finite state machines, labelled transition systems, Petri nets, vector addition systems, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as operational semantics, denotational semantics, axiomatic semantics and Hoare logic.
Within computer science, there are connections with abstract interpretation, program verification, and model checking.

Model checking

model checkermodel checkerssymbolic model checking
One approach and formation is model checking, which consists of a systematically exhaustive exploration of the mathematical model (this is possible for finite models, but also for some infinite models where infinite sets of states can be effectively represented finitely by using abstraction or taking advantage of symmetry).

Isabelle (proof assistant)

IsabelleIsabelle theorem proverIsabelle proof assistant
It consists of generating from the system and its specifications (and possibly other annotations) a collection of mathematical proof obligations, the truth of which imply conformance of the system to its specification, and discharging these obligations using either interactive theorem provers (such as HOL, ACL2, Isabelle, Coq or PVS), automatic theorem provers, or satisfiability modulo theories (SMT) solvers.
Isabelle has been used to aid formal methods for the specification, development and verification of software and hardware systems.

List of important publications in theoretical computer science

On Computable NumbersImportant publications in algorithmic information theoryImportant publications in computability
The tree automaton had numerous applications to proofs of correctness of programs.

Functional programming

functionalfunctional programming languagefunctional language
Another complementary approach is program derivation, in which efficient code is produced from functional specifications by a series of correctness-preserving steps.
Through the Curry–Howard isomorphism, then, well-typed programs in these languages become a means of writing formal mathematical proofs from which a compiler can generate certified code.

SystemVerilog

System VerilogConstrained random generation in SystemVerilogIEEE 1800
The properties to be verified are often described in temporal logics, such as linear temporal logic (LTL), Property Specification Language (PSL), SystemVerilog Assertions (SVA), or computational tree logic (CTL).
Most design teams cannot migrate to SystemVerilog RTL-design until their entire front-end tool suite (linters, formal verification and automated test structure generators) support a common language subset.

Dependent type

dependent typesdependently typeddependent
A promising type-based verification approach is dependently typed programming, in which the types of functions include (at least part of) those functions' specifications, and type-checking the code establishes its correctness against those specifications.
The code-generation aspect provides a powerful approach to formal program verification and proof-carrying code, since the code is derived directly from a mechanically verified mathematical proof.

Runtime verification

Aspect-oriented Programming
Runtime verification avoids the complexity of traditional formal verification techniques, such as model checking and theorem proving, by analyzing only one or a few execution traces and by working directly with the actual system, thus scaling up relatively well and giving more confidence in the results of the analysis (because it avoids the tedious and error-prone step of formally modelling the system), at the expense of less coverage.