Vo 8

• Specify the correct behavior of the unit under test

• Generate inputs e.g. using fuzzing

• Check wether the specification holds

Fully specifying large system is highly non-trivial:

-> it requires significant amounts of time and effort

1. Run multiple implementations

   • of the same functionality

   • on the same input

2. Compare their responses for disagreement

   • If a disagreement exists, then at least one implementation must be wrong (Or: only one of them can be right)

Pros:

• Does not require a specification of correct behavior

Cons:

• Requires more than one implementation

• It’s unclear which implementation is to blame for a disagreement

  (It could be that the majority is wrong and a single one correct)

There is a bug if outputs o and o' do not satisfy Ro(o,o')

-> e.g. if P simply returns the input, o' > o should hold when i' > i

• only requires defining metamorphic transformations

  (which is much easier than writing full/blown specifications)

• does not require the existence of multiple implementations

= the decision problem of determining wheter logical formulas are satifiable with respect to a set of background theories

SMT - The Satisfiability Modulo Theories

1. Given a seed, transform it to generate ONLY SAT instances

2. Detect a bug if solver returns UNSAT

1. Generate a random assignment for all free variables in F

2. Fragment F and populate initial pool