A Benchmark Suite with Semantics-Qualified Expected Verdicts for Formal Verification of IEC 61131-3 Programs

Reproducibility artifact for the manuscript A Benchmark Suite with Semantics-Qualified Expected Verdicts for Formal Verification of IEC 61131-3 Programs. The suite contains 117 benchmarks over 186 program variants (25 textual Ladder Diagram, 88 graphical Ladder Diagram, 58 Structured Text, 7 Function Block Diagram, 5 Sequential Function Chart, 3 Instruction List) across ten industrial domains. Each variant is an IEC 61131-3 program in PLCopen XML or Structured Text paired with a formal safety property, an expected verdict qualified by the scan-order, retained-state, and timer semantics it assumes, a recorded derivation method (expert, fault injection, or cross-tool consensus), and a triggering witness for every violation. 65 benchmarks are tool-confirmed and 52 are candidates whose verdicts depend on semantics or are not yet encoded for a second checker; the evidence/ directory holds the per-variant results, the semantics audit, the NuSMV translator, and the scripts that regenerate every number in the paper. Change from v1.2.0: v1.2.0 (10.5281/zenodo.23447432) also contained 58 benchmarks generated by language models. They are removed in this version and listed in evidence/removed_llm_generated_58.txt. The manuscript analyzes only the 117 benchmarks of this release. Benchmark data are released under CC BY 4.0; the schema, validator, runner, and adapters are released under the MIT license.