Definitions

Model checking.

Model checking tries to answer the following problem: Given a model of a system and a given specification, check exhaustively and automatically whether this model meets the given specification. Specification typically contains requirements that can include invariants, temporal logics, or other types of safety requirements such as the absence of critical states. Model checking is a set of algorithmic techniques for automatically verifying if a finite-state system verifies formal specifications. A model checker has many components: a modeling language, a requirements language, search algorithms, and a debugging feedback. Model checkers typically perform reachability analysis.

Probabilistic model checking.

Probabilistic model checkers are algorithms that perform model checking (automated verification that aims to establish the correctness of some specification) on probabilistic systems.

Reachability analysis.

Reachability analysis tries to answer to the following problem: Given a model of a system, a time length, a set of initial conditions (and a set of possible input in the case of control systems), give the set of all points of the state space that can be reached (visited) by the system in the given time-window. Reachability analysis is the process of computing the set of reachable states for a system. It can be performed on finite or infinite-state systems.

Stability analysis.

Stability analysis tries to answer the following problem: Given a dynamical system, what are the stability properties of its solutions. Many families of techniques are developed to answer this problem. A very classic one in control theory consists in Lyapunov methods. These methods look at the variation of certain function measures of the trajectory amplitude.

Synthesis.

Program synthesis tries to answer the following problem: Given a high-level specification, generate a program that provably satisfies this specification. Program synthesis is a set of automatic programming techniques that take as input a set of non-algorithmic statements expressed in an appropriate formal language (typically a logical calculus). In particular, controller synthesis programs automatically produce control policies for a given model of a system and given formal specifications required by the user.

Theorem proving.

Theorem proving tries to answer the following problem: Given a mathematical statement (theorem), can we automatically generate a proof of it? Theorem provers are programs that show that some statement (the conjecture) is a logical consequence of a set of statements (the axioms and hypotheses). The conjecture, hypotheses and axioms are expressed in a logical language (generally first order logic). The proofs produced by theorem provers describe a sequence of logical consequences drawn from the axioms and hypotheses, in a formal manner that can be understood and agreed upon by everyone, even other computer programs.