IEC 61131-3 래더 다이어그램을 위한 자동화된 검증기(verifier)는 다이어그램을 모델 체크어(model-checker) 입력으로 변환하여 안전성을 향상시킵니다. 하지만, 이들의 검증되지 않은 프런트엔드(front-end) 변환은 표준에서 벗어날 경우 잘못된 결과를 조용히 반환할 위험이 있습니다 (위반 사항 누락 또는 오탐지 발생). 우리는 K 프레임워크로 구축된 IEC 61131-3 래더 다이어그램의 실행 가능한 형식 의미론인 K-ESBMC를 통해 이 격차를 해소합니다. K-ESBMC는 접점(contacts), 코일(coils), 타이머(timers), 카운터(counters), 에지 블록(edge blocks) 및 유지 스캔 사이클(retentive scan cycle)을 모델링하며, 단일 정의로부터 인터프리터와 연역적 검증기(deductive verifier)를 모두 생성합니다. OpenPLC/Matiec과 스캔-스캔 단위로 검증된 K-ESBMC는 ESBMC Programmable Logic Controller (PLC) 래더 다이어그램을 GOTO 변환으로 차별적으로 테스트하기 위한 독립적인 참조 오라클(reference oracle) 역할을 합니다. 이는 대부분의 프로그램에서 ESBMC와 일치하며, 주입된 위반 사항들을 구체적인 증인(concrete witnesses)과 함께 재현합니다. 모든 불일치는 OpenPLC 및 다른 두 검증기에 의해 확인된 진정한 ESBMC 결함을 노출시키며, 두 가지 실패 모드를 밝혀냅니다: 안전하지 않은 프로그램을 인증하는 부적절한 건너뛰기(unsound skip), 그리고 허위 반례를 생성하는 부정확한 해복(imprecise havoc)입니다. 조합 논리 및 래치 조각(combinational and latch fragment)에 대해서는 kprove에서 기계 검사(machine-check)를 수행하여 K-ESBMC의 규칙이 표준의 입/출력 관계를 구현함을 보여주었고, 이를 통해 정확성 주장을 경험적 수준에서 형식적 수준으로 격상시켰습니다. K-ESBMC는 모든 래더 다이어그램 검증기의 변환을 감사(auditing)하기 위한 재사용 가능하고 표준에 충실한 오라클을 제공하며, 변환 기반 검증 도구의 건전성(soundness)을 검증하는 일반적인 접근 방식을 제시합니다.