ESBMC-LLB detects ladder logic bombs in PLC programs using formal verification

ESBMC-LLB is a tool that uses ESBMC-PLC+ to detect Ladder Logic Bombs (LLB) in IEC 61131-3 PLC programs by exposing function-block logic often dropped by existing verifiers. It recasts bomb detection as a formal verification problem, using k-induction for unbounded proof of bomb-absence and bounded model checking to recover triggers.

On the Iacobelli 2024 dataset, ESBMC-LLB detects all 30 bombs and recovers every trigger, including adaptive ones that evade CFG-triage. On PLC-Defuser's SWaT corpus v1.0.0, it detects 149/150 bombs (99%) with zero false positives, though detection drops to 49% on later versions with nonlinear non-termination bombs due to solver timeouts.

The authors conclude that semantic model checking and CFG-triage are complementary, with the former providing unbounded proofs and robustness against adaptive triggers.