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-삼분화가 상호 보완적이며, 전자가 무한 증명과 적응형 트리거에 대한 강건성을 제공한다고 결론지었습니다.