8 papers
K-ESBMC: An Executable Formal Semantics of IEC 61131-3 Ladder Diagram for Validating Verifier Translations
Pierre Dantas, Lucas Cordeiro, Waldir Junior
Automated verifiers for IEC 61131-3 ladder diagrams enhance safety by translating diagrams into model-checker inputs. Still, their unverified front-end translations risk silently r…
ESBMC-Arduino: Closing the Deployment Gap for Formal Verification of Open-Hardware PLCs
Pierre Dantas, Lucas Cordeiro, Waldir Junior
OpenPLC, Arduino OPTA, CONTROLLINO, and Industrial Shields M-Duino bring IEC 61131-3 to low-cost microcontrollers used in real automation and industrial control system (ICS) securi…
Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis
Pierre Dantas, Lucas Cordeiro, Waldir Junior
A Ladder Logic Bomb (LLB) is malicious control logic in a Programmable Logic Controller (PLC) program that lies dormant until a trigger activates a payload to manipulate actuators,…
ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Framework as a PLCverif Successor
Pierre Dantas, Lucas Cordeiro, Waldir Junior
PLCverif is the most mature open-source platform for PLC formal verification, developed at CERN and in production use since 2019. Yet it has two fundamental limitations: no support…
The 4/ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee
Pierre Dantas, Lucas Cordeiro, Youcheng Sun +1
The integration of Formal Verification tools with Large Language Models (LLMs) offers a path to scale software verification beyond manual workflows. However, current methods remain…
ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking
Pierre Dantas, Lucas Cordeiro, Waldir Junior
PLCopen XML defines two encoding formats for IEC 61131-3 Ladder Diagram programs: a textual encoding using <rung> elements, and a graphical encoding that represents rung logic as a…