FM Tools Data Schema

Predicate Abstraction is an abstract domain
in which abstract states represent a set of concrete states using predicated from a given set of predicates (called the precision).
The set of predicates is fixed for one abstraction computation, but can chance from location to location.
There are two kinds of predicate abstraction: cartesian predicate abstraction and boolean predicate abstraction.

Literature:

• 'Construction of Abstract State Graphs with PVS', Proc. CAV, 1997
• 'Boolean and Cartesian Abstraction for Model Checking C Programs', Proc. TACAS, 2001

Symbolic Execution is model-checking technique
in which a symbolic store assigns values to variables,
where the symbolic values can be constrained by a set of path constraints.

Literature:

• 'Symbolic Execution and Program Testing', Comm. ACM, 1976

Bounded Model Checking (BMC) is a model-checking technique
that unrolls the transition system a finite number of times.

Literature:

• 'Symbolic Model Checking without BDDs', Proc. TACAS, 1999
• 'Bounded Model Checking', Adv. Comput., 2003

k-Induction generalizes 1-induction.
1-Induction uses as premise that the property holds for the (one) previous object, while
k-induction generalizes it to using as premise that the property holds for the k previous objects.

Literature:

• 'The k-Induction Principle', Online, 2013
• 'PKind: A Parallel k-Induction Based Model Checker', EPTCS, 2011

Property-Directed Reachability is a model-checking technique
that constructs a sequence of invariants (also called frames)
that describe the reachable states after a number of transitions,
by continuously refining the invariants directed by paths that
reach a target state.

Literature:

• 'SAT-Based Model Checking Without Unrolling', Proc. VMCAI, 2011
• 'Property-Directed Incremental Invariant Generation', Formal Asp. Comput., 2008

Explicit-Value Analysis is a model-checking technique
that stores explicit values for program variables,
with similarities to constant-propagation data-flow analyses
and explicit-state model checking.

Literature:

• 'Explicit-State Model Checking', Handbook of Model Checking, 2018
• 'A Unified Approach to Global Program Optimization', Proc. POPL, 1973
• 'Explicit-State Software Model Checking Based on CEGAR and Interpolation', Proc. FASE, 2013

Numeric Interval Analysis is a data-flow analysis
that is based on the abstract domain of intervals,
in which each program variable is mapped to an interval of values.

Literature:

• 'Compiler Analysis of the Value Ranges for Variables', IEEE Trans. Software Eng., 1977
• 'Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints', Proc. POPL, 1977

Shape Analysis

Separation Logic provides reasoning about the heap,
which makes is particularly useful for verifying memory safety
and other properties that require the analysis of the program heap.

Literature:

• 'Separation Logic', Comm. ACM, 2019
• 'An Overview of Separation Logic', Proc. VSTTE, 2008
• 'Local Reasoning about Programs that Alter Data Structures', Proc. CSL, 2001

Bit-Precise Analysis is a technique in which the
abstract domain for tracking values treats variables of type int
as bit vectors, instead of approximating them as (unbounded) integers.

ARG-Based Analysis is a model-checking technique
that stores successor relations in the set of reached abstract states,
which is particularly useful for constructing error paths
once a violation of the specification is found.

Literature:

• 'The Software Model Checker Blast: Applications to Software Engineering', Int. J. Softw. Tools Technol. Transf., 2007

Lazy Abstraction is a technique from software model checking
that lazily refines the abstract model only when and where needed,
resulting in abstract models (ARGs) that can have different precisions
on different paths and on different locations on a path.

Literature:

• 'Lazy Abstraction', Proc. POPL, 2002
• 'The Software Model Checker Blast: Applications to Software Engineering', Int. J. Softw. Tools Technol. Transf., 2007

Interpolation is a technique from model checking
that computes for a two formulas A and C, for which A → C holds,
a new formula B such that A → B → C
and B contains only symbols that occur in A and C.

Literature:

• 'Linear Reasoning. A New Form of the Herbrand-Gentzen Theorem', J. Symb. Log., 1957
• 'Interpolation and SAT-Based Model Checking', Proc. CAV, 2003

Automata-Based Analysis is a technique from software model checking
in which automata are used in the analysis algorithm,
either to represent the abstract state space or the specification.

Literature:

• 'Software Model Checking for People Who Love Automata', Proc. CAV, 2013
• 'The BLAST Query Language for Software Verification', Proc. SAS, 2004

Concurrency Support comprises techniques
that make it possible to verify concurrent programs,
which use more than one execution thread and shared memory.

Ranking Functions are used to prove the termination of loops.
A ranking function maps the program's state to a well-founded set,
often the natural numbers, such that every loop iteration of the program
strictly decreases the value of the function.
If a ranking function for a loop can be found,
it guarantees that the loop terminates.

Literature:

• 'A Complete Method for the Synthesis of Linear Ranking Functions', Proc. VMCAI, 2004

Evolutionary Algorithms are heuristic optimization algorithms
that are inspired by biological evolution.
They use mechanisms such as mutation, crossover, and selection
to evolve a population of candidate solutions
towards an optimal or near-optimal solution.

Literature:

• 'Genetic Algorithms', Coll. Search Methodologies, 2005

Algorithm Selection is a technique that
inspects the input and based on information from the input
(for example, by extracting a feature vector) selects one
algorithm (that seems suited for the input)
from a set of given algorithms.

Literature:

• 'The Algorithm Selection Problem', Adv. Comput., 1976

Portfolio is a technique from economics
in which the risk is spread over several targets.
Algorithmic portfolios run several algorithms
in parallel or in sequence (while sharing resources),
in the hope that one of the algorithms finds the solution.

Literature:

• 'An Economics Approach to Hard Computational Problems', Science, 1997

Interpolation-Based Model Checking is a model-checking algorithm from 2003
that uses interpolants to over-approximate sets of reachable states.

Literature:

• 'Interpolation and SAT-Based Model Checking', Proc. CAV, 2003

Logic Synthesis

Literature:

• 'Advanced Logic Synthesis', Springer, 2018

Task Translation is a technique
that translates a verification task t into another verification task t'
such that an existing verification technique for t' can be used to derive
a verification result for t.

Literature:

• 'Testability Transformation', IEEE Trans. Softw. Eng., 2004

Floating-Point Arithmetics provides
precise reasoning about floating-point numbers in programs.
For example, expressions in the program can be translated
to SMT formulas using the theory of floating-point arithmetics.

Literature:

• 'Handbook of Floating-Point Arithmetic', Springer, 2018
• 'What Every Computer Scientist Should Know About Floating-Point Arithmetic', ACM Comput. Surv., 1991

Guidance by Coverage Measures is a technique
that uses coverage measures to guide the process of verification or test generation.

Random Execution is a technique for black-box testing
in which input values are randomly generated to construct
a test suite for the system under test.

Targeted Input Generation is a technique for software testing
that focuses on generating input values
that are likely to trigger specific behaviors or execution paths in the system.

CProver

ESBMC

JPF

Ultimate

JavaSMT

MathSAT

CVC

CSIsat

SMTinterpol

Z3

MiniSAT

Apron