Companion material for the phd thesis "formal specification and verification for automated production systems"

Abstract: This archive contains the evaluation for "Formal Specification and Verification for Automated Production Systems". In particular, you find evaluation environments for Chapter 7 (Evaluation (PART I - Generalized Test Tables)), 10 (Relational Test Tables), 11 (Provably Forgetting of Information), and 12 (Modular Regression Verification).

For more details, refer to the READMEs of the individual sub-folders. TechnicalRemarks: --------------------------------------------------------------------------------

 Formal Specification and Verification for Automated Production Systems

                            Alexander Weigl

                          COMPANTION MATERIAL

This bundle contains companion material for the PhD thesis "Formal Specification and Verification for Automated Production Systems". In particular you find following items:

1. Files of the evaluation of the chapters:
2. Chapter 07: Evaluation (PART I - Generalized Test Tables)
3. Chapter 10: Relational Test Tables
4. Chapter 11: Provably Forgetting of Information
5. Chapter 12: Modular Regression Verification

Runtime artefacts and log files are included.

Further details are given in the README.md files of the sub-directories.

1. Software for the evaluation
2. verifaps-lib: the developed library for the verification of automated production systems (GPL v3)
3. eldarica: used for verification of C files (BSD 3-clause license)
4. ic3ia: used for the of VMT files (generated by nuXmv) (GPL v3)

Not included and required for some experiments are

• nuXmv (Version: 1.1.1, and 2.0.0), model checker, not included due to license restrictions.

• SeaHorn, C program verifier, not included due to its large space size

  SeaHorn can be easly obtained by Docker or Podman:

  $ podman run -ti seahorn/seahorn-llvm10:nightly