ESBMC-LLB एक उपकरण है जो मौजूदा सत्यापक द्वारा अक्सर छोड़ दिए गए फ़ंक्शन-ब्लॉक तर्क को उजागर करके IEC 61131-3 PLC प्रोग्रामों में लैडर लॉजिक बम (LLB) का पता लगाने के लिए ESBMC-PLC+ का उपयोग करता है। यह बम सत्यापन को एक औपचारिक सत्यापन समस्या के रूप में फिर से परिभाषित करता है, बम की अनुपस्थिति के लिए असीमित प्रमाण के लिए k-इंडक्शन और ट्रिगर को पुनर्प्राप्त करने के लिए बाउंडेड मॉडल चेकिंग का उपयोग करता है।
Iacobelli 2024 डेटासेट पर, ESBMC-LLB सभी 30 बमों का पता लगाता है और हर ट्रिगर को पुनर्प्राप्त करता है, उन अनुकूली ट्रिगर सहित जो CFG-ट्रायज से बचते हैं। PLC-Defuser के SWaT कॉरपस v1.0.0 पर, यह 149/150 बमों (99%) का पता लगाता है, शून्य फॉल्स पॉजिटिव के साथ, हालांकि सॉल्वर टाइमआउट के कारण गैर-रेखीय नॉन-टरमिनेशन बम वाले बाद के संस्करणों पर पता लगाना 49% तक गिर जाता है।
लेखकों का निष्कर्ष है कि सेमांटिक मॉडल चेकिंग और CFG-ट्रायज पूरक हैं, जिसमें पहले वाला असीमित प्रमाण और अनुकूली ट्रिगर के खिलाफ दृढ़ता प्रदान करता है।