Applications

TBD: add usage examples

Testing

(Uniform) Sampling

Combinatorial Interation Testing (CIT):

CIT is a combinatorial testing technique that generates test cases by selecting a subset of the input parameters and their values. The goal is to cover all possible combinations of the input parameters. Pairwise testing is a special case of CIT where each test case covers all possible pairs of input parameters. When the parameters are constrained by logical formulas, CIT should generate input parameters that satisfy the constraints.

Constrained Random Testing (CRT): In hardware verification, CRT is used to generate test cases that satisfy the constraints of the design. This notion can be extended to software testing, where CRT is used to generate test cases that satisfy the constraints of the program.

Satisfiability Testing

Symbolic Execution
Hybrid Fuzzing

Optimization Modulo Theory

Symbolic Execution (Concretizing symbolic indexes)

Verification

Predicate Abstraction:
Bounded Model Checking and K-Induction
Symbolic Abstraction
…?

Synthesis

Optimizations

Superoptimization

Learning

Symbolic Regression
Learning Modulo Theory