[Artifact] Automated Invariant Generation for Efficient Deductive Reasoning about Embedded Systems

doi:10.4121/86963fe3-cc3f-45c3-b252-00d8780c4a1a.v2
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/86963fe3-cc3f-45c3-b252-00d8780c4a1a
Datacite citation style:
Philip Tasche; Paula Herber; Huisman, Marieke (2024): [Artifact] Automated Invariant Generation for Efficient Deductive Reasoning about Embedded Systems. Version 2. 4TU.ResearchData. dataset. https://doi.org/10.4121/86963fe3-cc3f-45c3-b252-00d8780c4a1a.v2
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite
Dataset
choose version:
version 2 - 2024-10-09 (latest)
version 1 - 2024-06-30

This is the artifact for the paper Automated Invariant Generation for Efficient Deductive Reasoning about Embedded Systems. It contains a version of the VerCors verifier and case studies for verification of SystemC designs. Each case study contains detailed instructions on transforming the SystemC source code to PVL, optimizing the PVL program and encoding properties, generating an invariant with VerCors and verifying the resulting system. All data is available in a prepackaged VM as well as separately in a .zip archive. Both username and password to the VM is "artifact".

history
  • 2024-06-30 first online
  • 2024-10-09 published, posted
publisher
4TU.ResearchData
format
VM image/ova; code/{cpp, h, pvl}; script/sh; text/md
organizations
University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science

DATA

files (1)