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

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