Abstraction-based Trace Generation to Validate Semantics of Formal Verifiers: Validation Model Suite

Dataset of the Scientific Students’ Association Report titled Abstraction-based Trace Generation to Validate Semantics of Formal Verifiers.

These files contain the validation model test suite and the generated traces. The models and traces are in the format of the Gamma modeling tool.

validation-model-suite/model/package/model contains the files for a given model:
- stm.gcd is the statemachine,
- default.ggen (and in Package F also abstraction.ggen) is the Gamma script executing trace generation and the generated traces can be found in the default (and abstraction) directories.
The report of Theta on possible coverage violation is in the traces directory (report.txt).

The prototype implementation of trace generation can be found at: https://github.com/AdamZsofi/gamma/tree/dev-tracegen