  Ladder Logics is a programming language standardized in IEC 61131-3 and
widely used for programming industrial Programmable Logic Controllers (PLC). A
PLC program consists of inputs (whose values are given at runtime by factory
sensors), outputs (whose values are given at runtime to factory actuators), and
the logical expressions computing output values from input values. Due to the
graphical form of Ladder programs, and the amount of inputs and outputs in
typical industrial programs, debugging such programs is time-consuming and
error-prone. We present, in this paper, a Why3-based tool prototype we have
implemented for automating the use of deductive verification in order to
provide an easy-to-use and robust debugging tool for Ladder programmers.
