Formal verification

In the context of (software) systems, formal verification means the act of proving or disproving the correctness of a system with respect to a certain property, using mathematical methods.

System types that are considered in the literature for formal verification include finite state machines (FSM), labelled transition systems (LTS) and their compositions, Petri nets, timed automata and hybrid automata, cyptographic protocols, combinatorial circuits, digital circuits with internal memory, and abstractions of general software components.

The properties to be verified are often described in temporal logics, such as linear-time temporal logic (LTL) or computational tree logic (CTL).

Usually formal verification is carried out algorithmically. The main approaches to implementing formal verification include state space enumeration, symbolic state space enumeration, abstraction refinement, process-algebraic methods, and reasoning with the aid of automatic theorem provers such as HOL or Isabella.