A Benchmark Suite and Ground-Truth Methodology for Formal Verification of IEC 61131-3 Ladder Diagram Programs

Reproducibility artifact for the manuscript A Benchmark Suite and Ground-Truth Methodology for Formal Verification of IEC 61131-3 Ladder Diagram Programs. The suite contains 50 benchmarks over 83 program variants (15 textual Ladder Diagram, 25 graphical Ladder Diagram, 10 Structured Text) across ten industrial domains, each an IEC 61131-3 program in standard PLCopen XML or Structured Text paired with a formal safety property, a machine-checkable expected verdict, a recorded ground-truth method, and, for every violation, a triggering witness. It is, to our knowledge, the first formal-verification benchmark suite to cover graphical Ladder Diagram, the encoding in which real programs are exchanged. Ground truth for every verdict is established by one of three methods — construction (expert), fault injection, or audited cross-tool consensus — and the method used is recorded per variant. Each benchmark also records a validation_status: 31 benchmarks are tool-confirmed (ESBMC-PLC+ and/or nuXmv) and 19 are candidates whose verdicts are semantics-dependent or not yet encoded for a second checker. The corpus is packaged in an SV-COMP-compatible layout and ships with a JSON Schema, a schema validator (runner/validate.py), tool adapters, and a one-command re-check harness, so a new tool is added through an adapter rather than by reformatting the corpus. Benchmark data are released under CC BY 4.0; the schema, validator, runner, and adapters are released under the MIT licence.