What is Formal Verification

The use of formal methods to ensure that a set of properties are valid in a given system under test.

Application of formal methods to establish the correctness of a system.

A verification methodology for mathematically proving the compliance of a design against a formally defined logical specification.

The process of checking whether a design satisfies some system properties (requirements). In order to formally verify a design, it must first be converted into a simpler “verifiable” format. The design is specified as a set of interacting systems; each has a finite number of configurations, called states. States and transition between states constitute Finite State Machines (FSMs). The entire system is an FSM, which can be obtained by composing the FSMs associated with each component. Hence the first step in verification consists of obtaining a complete FSM description of the system. Given a present state (or current configuration), the next state (or successive configuration) of an FSM can be written as a function of its present state and inputs (transition function or transition relation).

An act of proving or disproving, using mathematically-based techniques, the correctness of intended algorithms underlying a system with respect to a certain formal specification or property.