FM Tools Data Schema

C is a general purpose programming language.

Java is a general purpose programming language.

SV-LIB is an SMT-LIB-based exchange format for imperative programs.

Python is a general purpose programming language.

MoXI (Model eXchange Interlingua) is an SMT-LIB-based intermediate language for symbolic model checking.

Btor2 is a word-level format for expressing model-checking problems in sequential circuits over bit-vectors and arrays.

SMV is a formal modeling language for symbolic transition systems and temporal properties.

VMT-LIB is an SMT-LIB-based language for describing symbolic transition systems and properties.

DIMACS CNF is the standard exchange format for propositional satisfiability (SAT) problems.

GRAT is an unsat certificate format produced by SAT solvers and verified by proof checkers such as GRATchk.

Pseudo-Boolean is an input format for pseudo-boolean optimization and satisfiability problems.

Counter-Example Guided Inductive Synthesis

Literature:

• 'Decision Tree Learning in CEGIS-Based Termination Analysis', Proc. CAV, 2021

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.

Template-Based Predicate Inference is a technique for software verification
that synthesizes predicates to be added to the precision of predicate abstraction
by trying to instantiate predicates (e.g., invariants) from a given set of templates.

Deductive Verification

Abstract Interpretation is a mathematical framework used to define and prove the soundness of abstractions.
In static analysis, it allows one to soundly approximate program semantics using abstract domains,
thereby automatically inferring invariants to verify program properties without executing the program.

Literature:
- 'Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints', Proc. POPL, 1977
- 'Systematic design of program analysis frameworks', Proc. POPL, 1978

Fuzzing is a dynamic software testing technique
that automatically generates a large number of random or semi-random inputs
to test programs for bugs, vulnerabilities, and crashes.
It is particularly effective at finding security vulnerabilities and robustness issues.

Literature:
- 'The Fuzzing Book', Online, 2023

Constrained Horn Clauses (CHC) is a technique to transform transition systems
into Horn clauses with constraints from a background theory and
delegate the actual verification to CHC solvers.

Literature:
- 'Horn Clause Solvers for Program Verification', Proc. Festschrift 75th Birthday Yuri Gurevich

CProver

ESBMC

JPF

Ultimate

Eldarica

Golem

JavaSMT

MathSAT

CVC

CSIsat

SMTinterpol

Z3

PCSat

PySMT

MiniSAT

Glucose

Apron

Viper

LiSA

AFL++ (American Fuzzy Lop Plus Plus)

Bitwuzla

Boolector

Smt-Switch

Yices2

Klee is a symbolic executor of LLVM IR code.

Symbiotic is a program analysis framework integrating scripts for compilation and various
3rd party libraries and tools for program slicing, point-to analysis, and verification.

Frama-C is an open-source, extensible platform dedicated to the source-code analysis of
C software. It integrates several analysis techniques, including abstract interpretation,
deductive verification, and runtime verification.

Astral is a solver for various fragments of separation logic with inductive definitions.
Its approach is based on a translation to SMT, allowing it to leverage multiple existing
SMT solvers as backends.

Goblint is an abstract interpretation framework that
is dedicated to the sound thread-modular analysis of multi-threaded
programs, especially for data races.