2026-10-10T07:58:50Zhttps://www.radar-service.eu/oai/OAIHandler10.35097/15372026-10-09T10:49:10Zradar4kit
https://dx.doi.org/10.35097/1537
Weigl, Alexander
Companion Material for the PhD thesis "Formal Specification and Verification for Automated Production Systems"
Karlsruhe Institute of Technology
2023
Computer Science
dataset
Dataset
info:eu-repo/semantics/openAccess
https://creativecommons.org/licenses/by-nc-sa/4.0/legalcode
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.
--------------------------------------------------------------------------------
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:
* 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.
2. 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`](https://nuxmv.fbk.eu) (Version: 1.1.1, and 2.0.0),
model checker, not included due to license restrictions.
* [`SeaHorn`](https://seahorn.github.io/),
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
```
Formal Specification
Formal Verification
Automated Production Systems
Manufacturing Systems
nuXmv
IC3
Eldarica
SeaHorn
10.5445/IR/1000139656
KITopen-DOI
application/x-tar