In the context of hardware and software systems, formal verification is the act of proving

Mathematical proof

In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...

 or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification

Formal specification

In computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it...

 or property, using formal methods

Formal methods

In computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...

 of mathematics

Mathematics

Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...

 .

Usage

Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocol

Cryptographic protocol

A security protocol is an abstract or concrete protocol that performs a security-related function and applies cryptographic methods.A protocol describes how the algorithms should be used...

s, combinational circuit

Combinational logic

In digital circuit theory, combinational logic is a type of digital logic which is implemented by boolean circuits, where the output is a pure function of the present input only. This is in contrast to sequential logic, in which the output depends not only on the present input but also on the...

s, digital circuit

Digital circuit

Digital electronics represent signals by discrete bands of analog levels, rather than by a continuous range. All levels within a band represent the same signal state...

s with internal memory, and software expressed as source code.

The verification of these systems is done by providing a formal proof

Formal proof

A formal proof or derivation is a finite sequence of sentences each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system...

 on an abstract mathematical model

Mathematical model

A mathematical model is a description of a system using mathematical concepts and language. The process of developing a mathematical model is termed mathematical modeling. Mathematical models are used not only in the natural sciences and engineering disciplines A mathematical model is a...

 of the system, the correspondence between the mathematical model and the nature of the system being otherwise known by construction. Examples of mathematical objects often used to model systems are: finite state machine

Finite state machine

A finite-state machine or finite-state automaton , or simply a state machine, is a mathematical model used to design computer programs and digital logic circuits. It is conceived as an abstract machine that can be in one of a finite number of states...

s, labelled transition systems, Petri net

Petri net

A Petri net is one of several mathematical modeling languages for the description of distributed systems. A Petri net is a directed bipartite graph, in which the nodes represent transitions and places...

s, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as operational semantics

Operational semantics

In computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Operational semantics are classified into two categories: structural operational semantics formally describe how the individual steps of a computation take place in a...

, denotational semantics

Denotational semantics

In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...

, axiomatic semantics

Axiomatic semantics

Axiomatic semantics is an approach based on mathematical logic to proving the correctness of computer programs. It is closely related to Hoare logic....

 and Hoare logic

Hoare logic

Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...

.

Approaches to formal verification

One approach and formation is model checking

Model checking

In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....

, 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 using abstraction). Usually this consists of exploring all states and transitions in the model, by using smart and domain-specific abstraction techniques to consider whole groups of states in a single operation and reduce computing time. Implementation techniques include state space enumeration

State space enumeration

In computer science, state space enumeration are methods that consider each reachable program state to determine whether a program satisfies a given property. As programs increase in size and complexity, the state space grows exponentially. The state space used by these methods can be reduced by...

, symbolic state space enumeration, abstract interpretation

Abstract interpretation

In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics In...

, symbolic simulation

Symbolic simulation

In computer science, a simulation is a computation of the execution of some appropriately modelled state-transition system. Typically this process models the complete state of the system at individual points in a discrete linear time frame, computing each state sequentially from its predecessor...

, abstraction refinement. The properties to be verified are often described in temporal logic

Temporal logic

In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. In a temporal logic we can then express statements like "I am always hungry", "I will eventually be hungry", or "I will be hungry...

s, such as linear temporal logic

Linear temporal logic

In logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...

 (LTL) or computational tree logic

Computational tree logic

Computation tree logic  is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realised...

 (CTL).

Another approach is logical inference. It consists of using a formal version of mathematical reasoning about the system, usually using theorem proving software such as a HOL theorem prover

HOL theorem prover

HOL denotes a family of interactive theorem proving systems sharingsimilar logics and implementation strategies....

, the ACL2, Isabelle, or Coq

Coq

In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...

 theorem provers. This is usually only partially automated and is driven by the user's understanding of the system to validate. Recent tools such as Perfect Developer

Perfect Developer

Perfect Developer is a tool for developing computer programs in a rigorous manner. It is used to develop applications in areas including IT systems and airborne critical systems. The principle is to develop a formal specification and refine the specification to code...

 and Escher C Verifier attempt to automate the proof process fully.

"Non-classical" logics such as linear logic

Linear logic

Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...

 and temporal logics can also be used in logical inference, not just in model checking.

Formal verification for software

Logical inference for the formal verification of software can be further divided into:

• the more traditional 1970s approach in which code is first written in the usual way, and subsequently proven correct in a separate step;
• 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. Fully featured dependently typed languages support the first approach as a special case.

A slightly different (and complementary) approach is program derivation

Program derivation

In computer science, program derivation is the derivation of a program from its specification, by mathematical means.To derive a program means to write a formal specification, which is usually non-executable, and then apply mathematically correct rules in order to obtain an executable program...

, in which efficient code is produced from functional

Functional programming

In computer science, functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids state and mutable data. It emphasizes the application of functions, in contrast to the imperative programming style, which emphasizes changes in state...

 specifications by a series of correctness-preserving steps. An example of this approach is the Bird-Meertens Formalism

Bird-Meertens Formalism

The Bird-Meertens Formalism is a calculus for deriving programs from specifications , devised by Richard Bird and Lambert Meertens....

, and this approach can be seen as another form of correctness by construction.

Verification and validation

Verification

Verification

The word verification may refer to:* Verification and validation, in engineering or quality management systems, it is the act of reviewing, inspecting or testing, in order to establish and document that a product, service or system meets regulatory or technical standards.* Verification , in the...

 is one aspect of testing a product's fitness for purpose. Validation is the complementary aspect. Often one refers to the overall checking process as V & V

Verification and Validation

In software project management, software testing, and software engineering, verification and validation is the process of checking that a software system meets specifications and that it fulfills its intended purpose...

.

• Validation: "Are we trying to make the right thing?", i.e., is the product specified to the user's actual needs?
• Verification: "Have we made what we were trying to make?", i.e., does the product conform to the specifications?

The verification process consists of static/structural and dynamic/behavioral aspects. E.g., for a software product one can inspect the source code (static) and run against specific test cases (dynamic). Validation usually can be done only dynamically, i.e., the product is tested by putting it through typical and atypical usages ("Does it satisfactorily meet all use case

Use case

In software engineering and systems engineering, a use case is a description of steps or actions between a user and a software system which leads the user towards something useful...

s?").

Industry usage

The growth in complexity of designs increases the importance of formal verification techniques in the hardware industry. At present, formal verification is used by most or all leading hardware companies, but its use in the software industry is still languishing. This could be attributed to the greater need in the hardware industry, where errors have greater commercial significance. Because of the potential subtle interactions between components, it is increasingly difficult to exercise a realistic set of possibilities by simulation. Important aspects of hardware design are amenable to automated proof methods, making formal verification easier to introduce and more productive.

, several operating systems have been formally verified:
NICTA's Secure Embedded L4 microkernel, sold commercially as seL4 by OK Labs; Green Hills Software's Integrity operating system

Integrity (operating system)

INTEGRITY is a real-time operating system produced and marketed by Green Hills Software. It is royalty-free, POSIX-certified, and intended for use in embedded systems needing reliability, availability, and fault tolerance. It is built atop the velOSity microkernel and is intended mainly for modern...

; and SYSGO

SYSGO

SYSGO AG is a German company oriented in embedded software since its founding in 1991. The company is focused on the basic software building blocks for embedded systems used in critical environments such as airplanes, medical instruments or industrial automation...

's PikeOS

PikeOS

PikeOS is a microkernel-based real-time operating system made by SYSGO AG. It is targeted at safety and security critical embedded systems. It provides a partitioned environment for multiple operating systems with different design goals, safety requirements, or security requirements to coexist in a...

.

See also

• Automated theorem proving
  Automated theorem proving
  Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
  
  
• Formal equivalence checking
  Formal equivalence checking
  Formal equivalence checking process is a part of electronic design automation , commonly used during the development of digital integrated circuits, to formally prove that two representations of a circuit design exhibit exactly the same behavior....
  
  
• LURCH
  LURCH
  LURCH is a tool for software design debugging that uses a nondeterministic algorithm to quickly explore the reachable states of a software model...
  
  
• Proof checker
• Property Specification Language
  Property Specification Language
  Property Specification Language is a language developed by Accellera for specifying properties or assertions about hardware designs. The properties can then be simulated or formally verified. Since September 2004 the standardization on the language has been done in IEEE 1850 working group...
  
  
• Selected formal verification bibliography
• Static code analysis
  Static code analysis
  Static program analysis is the analysis of computer software that is performed without actually executing programs built from that software In most cases the analysis is performed on some version of the source code and in the other cases some form of the object code...
  
  
• Temporal logic in finite-state verification
  Temporal logic in finite-state verification
  In finite-state verification, model checkers examine finite-state machines representing concurrent software systems looking for errors in design. Errors are defined as violations of requirements expressed as properties of the system...
  
  
• Post silicon validation
  Post silicon validation
  Post-silicon validation and debug is the last step in the development of a semiconductor integrated circuit. During the pre-silicon process, engineers test devices in a virtual environment with sophisticated simulation, emulation, and formal verification tools...
  
  
• Intelligent verification
  Intelligent verification
  Intelligent Verification, also referred to as intelligent testbench automation, is a form of functional verification used to verify that an electronic hardware design conforms to specification before device fabrication...
  
  
• Runtime verification
  Runtime verification
  Runtime verification is a computing system analysis and execution approach based on extracting information from a running system and using it to detect and possibly react to observed behaviors satisfying or violating certain properties...