[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".本数据集为论文《面向嵌入式系统高效演绎推理的自动化不变量生成》（Automated Invariant Generation for Efficient Deductive Reasoning about Embedded Systems）的配套科研工件。数据集包含VerCors验证器（VerCors verifier）的可用版本，以及用于SystemC设计验证的案例集。每一则案例均附带详细操作指南，涵盖将SystemC源代码转换为PVL语言、优化PVL程序与编码验证属性、借助VerCors验证器生成不变量，以及对最终系统完成验证的全流程步骤。所有数据集既可通过预封装虚拟机（prepackaged VM）获取，也可单独通过.zip压缩包下载。该虚拟机的用户名与密码均为"artifact"。