ESBMC-LLB adalah alat yang menggunakan ESBMC-PLC+ untuk mendeteksi Bom Logika Tangga (LLB) dalam program PLC IEC 61131-3 dengan mengekspos logika blok-fungsi yang sering terlewat oleh verifier yang ada. Alat ini memetakan ulang deteksi bom sebagai masalah verifikasi formal, menggunakan induksi-k untuk pembuktian tanpa batas ketiadaan bom dan pemeriksaan model terbatas untuk memulihkan pemicu.
Pada dataset Iacobelli 2024, ESBMC-LLB mendeteksi semua 30 bom dan memulihkan setiap pemicu, termasuk yang adaptif yang menghindari triase CFG. Pada korpus SWaT v1.0.0 dari PLC-Defuser, alat ini mendeteksi 149/150 bom (99%) dengan nol false positive, meskipun deteksi turun menjadi 49% pada versi selanjutnya yang memiliki bom nonlinier non-terminasi karena timeout solver.
Para penulis menyimpulkan bahwa pemeriksaan model semantik dan triase CFG bersifat komplementer, dengan yang pertama menyediakan pembuktian tanpa batas dan ketahanan terhadap pemicu adaptif.