Citing¶
Cite the archived release rather than this site. The pages are the readable face of the artifact; the citable object is the versioned archive on Zenodo.
| title | A Benchmark Suite with Semantics-Qualified Expected Verdicts for Formal Verification of IEC 61131-3 Programs |
| authors | Pierre Dantas; Lucas C. Cordeiro; Waldir Junior |
| version | 1.3.3 |
| license | CC-BY-4.0 |
| DOI | 10.5281/zenodo.21642385 (version-independent doi, always resolving to the latest release) |
| DOI | 10.5281/zenodo.23848846 (doi of the archived v1.3.2 release) |
| DOI | 10.5281/zenodo.23783784 (doi of the archived v1.3.1 release) |
| DOI | 10.5281/zenodo.23447432 (doi of the archived v1.2.0 release (also holds 58 language-model benchmarks removed in v1.3.0)) |
| DOI | 10.5281/zenodo.22257881 (doi of the archived v1.1.1 release) |
| DOI | 10.5281/zenodo.22252807 (doi of the archived v1.1.0 release) |
| DOI | 10.5281/zenodo.21642386 (doi of the archived v1.0.1 release) |
A suite of 117 IEC 61131-3 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 paired with a formal safety property, an expected verdict qualified by the semantics it assumes, a recorded derivation method, and a triggering witness for every violation. Packaged in an SV-COMP-compatible layout with a JSON Schema, validator, tool adapters, and a one-command re-check harness.
@misc{dantas133,
title = {A Benchmark Suite with Semantics-Qualified Expected Verdicts for Formal Verification of IEC 61131-3 Programs},
author = {Dantas, Pierre and Cordeiro, Lucas C. and Junior, Waldir},
year = {2026},
doi = {10.5281/zenodo.21642385},
version = {1.3.3},
note = {Benchmark suite artifact}
}
The first DOI always resolves to the newest release. The others pin a specific version.
Cite whichever pinned DOI matches the release you actually measured against, not the
version-independent one, because that one can start resolving to a release that no longer
contains the task you measured. The manuscript under review reports release v1.3.2, so a
citation of that paper should pin 10.5281/zenodo.23848846. Release v1.2.0 also holds 58
benchmarks generated by language models, which the paper excludes.
Zenodo's own page for the v1.1.1 and v1.1.0 archives describes v1.0.1's content: its
metadata is generated from .zenodo.json at archival time, and that file lagged the
tree for those two releases. The archived tarball itself is the correct release; the
description on Zenodo's page is what is wrong, and only for those two entries.
An accompanying article is under review at Scientific Reports. CITATION.cff in the
repository carries its details and stays current; this page is generated from that file.