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:
- Files of the evaluation of the chapters:
- Chapter 07: Evaluation (PART I - Generalized Test Tables)
- Chapter 10: Relational Test Tables
- Chapter 11: Provably Forgetting of Information
- 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.
- Software for the evaluation
verifaps-lib
: the developed library for the verification of automated
production systems (GPL v3)
eldarica
: used for verification of C files (BSD 3-clause license)
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
BibTex: