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. 47 benchmarks are validated, with every variant on two ESBMC routes in the retained evidence, and 70 are candidates; 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 (DeepSeek and Gemini). 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. Change from v1.3.0: the evidence is rerun with the released ESBMC 8.6.0 in place of a development build; benchmarks, properties, and expected verdicts are unchanged. Change from v1.3.1: the semantics record evidence/semantics.yml is corrected (77 benchmarks retain state, not 56) and the g_two_hand descriptor no longer claims a synchronous-actuation window it does not model. evidence/revision/ adds the translation checks, second-engine runs, standards review, model reviews, and second-machine timings reported in the revision. Benchmarks, properties, and expected verdicts are unchanged. Change from v1.3.2: 18 benchmarks change from validated to candidate because the retained evidence does not show both ESBMC routes on every variant (evidence/validation_status_v1.3.3.csv); programs, properties, and expected verdicts are unchanged. Benchmark data are released under CC BY 4.0; the schema, validator, runner, and adapters are released under the MIT license.