Graph-ESBMC-PLC обеспечивает формальную проверку графических программ IEC 61131-3 на языке схем (Ladder Diagram) за счет введения разрешителя на основе поиска в глубину, который преобразует графические соединения LD в допустимую промежуточную форму представления GOTO. Проверка на трех реальных программах показывает полное генерирование IR и успешную проверку свойств безопасности при k=2 за 70 мс, без регрессии на текстовых бенчмарках.