TY - DATA
T1 - [Artifact] Automated Invariant Generation for Efficient Deductive Reasoning about Embedded Systems
PY - 2024/06/30
AU - Philip Tasche
AU - Paula Herber
AU - Marieke Huisman
UR - 
DO - 10.4121/86963fe3-cc3f-45c3-b252-00d8780c4a1a.v1
KW - deductive verification
KW - invariant generation
KW - embedded systems
KW - SystemC
KW - VerCors
N2 - <p>This is the artifact for the paper <em>Automated Invariant Generation for Efficient Deductive Reasoning about Embedded Systems</em>. 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".</p>
ER -