ESBMC-LLB é uma ferramenta que usa ESBMC-PLC+ para detectar Bombas de Lógica Escada (LLB) em programas PLC IEC 61131-3 expondo a lógica de blocos funcionais frequentemente ignorada por verificadores existentes. Ele reformula a detecção de bombas como um problema de verificação formal, usando indução k para provas ilimitadas de ausência de bombas e verificação limitada de modelos para recuperar gatilhos.
No conjunto de dados Iacobelli 2024, o ESBMC-LLB detecta todas as 30 bombas e recupera cada gatilho, incluindo os adaptativos que evitam a triagem de CFG. No corpus SWaT v1.0.0 do PLC-Defuser, ele detecta 149/150 bombas (99%) com zero falsos positivos, embora a detecção caia para 49% em versões posteriores com bombas não lineares sem término devido a tempos limite do solucionador.
Os autores concluem que a verificação de modelos semânticos e a triagem de CFG são complementares, fornecendo a primeira provas ilimitadas e robustez contra gatilhos adaptativos.