[Artifact] Deductive Verification of Parameterized Embedded Systems modeled in SystemC

doi: 10.4121/a7e780c9-87fa-486c-b484-a76a459a9d53.v1
The doi above is for this specific version of this dataset, which is currently the latest. Newer versions may be published in the future. For a link that will always point to the latest version, please use
doi: 10.4121/a7e780c9-87fa-486c-b484-a76a459a9d53
Datacite citation style:
Philip Tasche; Monti, Raúl E.; Drerup, Stefanie Eva; Blohm, Pauline; Paula Herber et. al. (2023): [Artifact] Deductive Verification of Parameterized Embedded Systems modeled in SystemC. Version 1. 4TU.ResearchData. software. https://doi.org/10.4121/a7e780c9-87fa-486c-b484-a76a459a9d53.v1
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite

This is the artifact for the paper Deductive Verification of Parameterized Embedded Systems modeled in SystemC. It contains software that enables the deductive verification of SystemC designs by transforming SystemC to PVL, as well as software to automatically generate global invariants that aid in deductive verification of global properties. Furthermore, the artifact contains files that support the paper's experiments. It contains SystemC case studies and pre-generated PVL translations that were used in the experiments. It also contains detailed instructions for general use of the included tools and for the replication of the experiments. For this, see the included README.pdf.

The artifact files are packaged in a VirtualBox virtual machine running Ubuntu 22.04.3 LTS, with all requirements pre-installed. Both username and password for the virtual machine image are "artifact" (without quotes). In addition to this, the relevant files of the artifact are also packaged in a separate .zip file.

All files contained in the artifact are licensed under the Mozilla Public License Version 2.0.

  • 2023-09-19 first online, published, posted
VM image/ova; code/{cpp, h, pvl, java, py}; application/jar; text/pdf
University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS), Formal Methods and Tools (FMT); University of Münster, Department of Mathematics and Computer Science, Embedded Systems (EmbSys)


files (1)