The DOI displayed 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

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

Version 1 - 2024-06-30

Usage statistics

Categories

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

Keywords

deductive verification embedded systems invariant generation SystemC VerCors

Licence

MPL 2.0

Export as...

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

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