Formal verification

In the context of software systems,\nformal verification is the act of\nproving or disproving the correctness of a system\nwith respect to a certain property,\nusing mathematical methods. System types that are considered in the literature for formal verification\ninclude finite state machines (FSM),\nlabelled transition systems (LTS) and\ntheir compositions,\nPetri nets, timed automata and hybrid automata,\ncryptographic protocols,\ncombinatorial circuits,\ndigital circuits with internal memory,\nand abstractions of general software components. The properties to be verified are often described\nin temporal logics, such as linear-time temporal logic (LTL) or computational tree logic (CTL). Usually formal verification is carried out algorithmically.\nThe main approaches to implementing formal verification\ninclude state space enumeration, symbolic state space enumeration, abstract interpretation,\nabstraction refinement, process-algebraic methods,\nand reasoning with the aid of automatic theorem provers such as\nHOL or Isabelle. \n

See also

\n*Important publications in formal verification\n*Scalable Program Analysis\n*Specification patterns for finite-state verification\n*Temporal logic in finite-state verification\n*LURCH