ESBMC-LLB هو أداة تستخدم ESBMC-PLC+ للكشف عن قنابل المنطق السلماني (LLB) في برامج PLC المعيارية IEC 61131-3 من خلال كشف منطق كتلة الوظائف الذي غالباً ما تتجاهله أدوات التحقق الحالية. يعيد صياغة مشكلة الكشف عن القنابل كمشكلة تحقق رسمي، باستخدام الاستقراء-k لإثبات عدم وجود القنابل بشكل غير محدود، واستخدام فحص النموذج المحدود لاستعادة المحفزات.
على مجموعة بيانات Iacobelli 2024، يكتشف ESBMC-LLB جميع القنابل الـ30 ويعيد كل محفز، بما في ذلك تلك المتكيفة التي تتجنب الفرز القائم على رسم تدفق التحكم (CFG). على مجموعة بيانات SWaT الإصدار v1.0.0 من PLC-Defuser، يكتشف 149 من أصل 150 قنبلة (99%) مع عدم وجود إيجابيات كاذبة، على الرغم من انخفاض معدل الكشف إلى 49% في الإصدارات اللاحقة التي تحتوي على قنابل غير خطية وغير متوقفة بسبب انتهاء مهلة المُحلل.
يستنتج المؤلفون أن فحص النموذج الدلالي وفرز CFG مكملان لبعضهما البعض، حيث يوفر الأول إثباتات غير محدودة ومتانة ضد المحفزات المتكيفة.