ESBMC-LLBは、既存の検証器でしばしば見落とされるファンクションブロックのロジックを明らかにすることにより、IEC 61131-3 PLCプログラム内のラダーロジックボム（LLB）を検出するためにESBMC-PLC+を利用するツールです。爆発物の検出を形式検証問題として再構築し、爆発物の不在の無制限な証明にはk帰納法を、トリガーの回復には有界モデル検査を使用します。

Iacobelli 2024データセットにおいて、ESBMC-LLBは30個のすべてのボムを検出し、CFGトライアージュを回避する適応型を含むすべてのトリガーを回復しました。PLC-DefuserのSWaTコーパスv1.0.0では、150個中149個のボム（99%）を検出し、偽陽性はゼロでしたが、ソルバーのタイムアウトにより非線形非終了ボムを持つ後続バージョンでの検出率は49%に低下しました。

著者らは、セマンティックモデル検査とCFGトライアージュは補完的であり、前者が無制限な証明と適応型トリガーに対する堅牢性を提供すると結論付けています。