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:
Tools:
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:
Tools:
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:
Tools:
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.
Tools:
Bounded Model Checking (BMC) is a model-checking technique that unrolls the transition system a finite number of times.
Literature:
Tools:
CounterExample-Guided Abstraction Refinement is a model-checking technique that iteratively refines the abstract model of the transition system by analyzing spurious counterexamples and learning a more precise abstraction.
Literature:
Tools:
Concurrency Support comprises techniques that make it possible to verify concurrent programs, which use more than one execution thread and shared memory.
Tools:
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:
Tools:
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:
Tools:
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:
Tools:
Guidance by Coverage Measures is a technique that uses coverage measures to guide the process of verification or test generation.
Tools:
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:
Tools:
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:
Tools:
Logic Synthesis
Literature:
Tools:
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:
Tools:
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:
Tools:
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:
Tools:
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:
Tools:
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.
Tools:
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:
Tools:
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:
Tools:
Shape Analysis
Tools:
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:
Tools:
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.
Tools:
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:
Tools:
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:
Tools:
