ESBMC-PLC는 IEC 61131-3 표준의 Ladder Diagram (LD) 프로그램 형식 검증을 위한 새로운 오픈소스 도구입니다. 기존 SMT 기반 모델 검증기에서 LD의 그래픽 표현을 처리할 수 없었던 한계를 극복했습니다.
PLC scan cycle을 모델링하고 안전 속성을 검증하는 방식으로, 5가지 속성 YAML 언어를 사용해 시간 논리 없이 검증 가능합니다.
13개의 벤치마크 평가 결과, 9개의 프로그램에서 예상대로 동작했으며 8개의 버그를 발견하고 7개의 unbounded k-induction 증명을 완료했습니다.