Software Verification Competition

新的基准测试套件旨在对工业PLC程序进行形式化验证

研究人员开发了一个新的基准测试套件，用于形式化验证IEC 61131-3梯形图程序，解决了该领域缺乏标准评估工具的问题。该套件包含来自十个工业领域的50个程序，以图形化（梯形图）和文本化（结构化文本）两种格式呈现。一项关键贡献是建立了一个地面实况方法，以确保可靠的判断，这些判断通过构造、故障注入或审计的跨工具共识来确立。该语料库、模式、验证器和复查工具被作为开放工件发布，以促进可复现的进展度量。