Philip Tasche; Paula Herber; Huisman, Marieke (2024): [Artifact] Automated Invariant Generation for Efficient Deductive Reasoning about Embedded Systems. Version 1. 4TU.ResearchData. dataset. https://doi.org/10.4121/86963fe3-cc3f-45c3-b252-00d8780c4a1a.v1

Dataset

x choose version: version 2 - 2024-10-09 (latest)

• Computer Software
• Other Technology
• Technology
• Information and Computing Sciences

deductive verification, embedded systems, invariant generation, SystemC, VerCors

MPL 2.0

RefWorks, BibTeX, Reference Manager, Endnote, DataCite, NLM, DC, CFF

by Philip Tasche , Paula Herber , Marieke Huisman

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".

• 2024-06-30 first online, published, posted

4TU.ResearchData

VM image/ova; code/{cpp, h, pvl}; script/sh; text/md

University of Twente, Faculty of Electrical Engineering, Mathematics and Computer ScienceI