At Vitens, the biggest drinking water company from the Netherlands, most processes in extracting, purifying and delivering drinking water are automated using PLCs. In order to check PLC programs, translation schemes for the programming languages Function Block Diagram and Structured Text are defined into an SMT solver. Using the SMT solver, a set of typical properties could be checked on a PLC program with the size typical for PLC programs within Vitens. Most properties could be shown to hold (and all could be (dis)proven in matters of seconds), although virtually all initially formulated properties required fine tuning before they could be shown valid.

The overall conclusion is that the use of SMT solvers is very effective in analysing industrial scale PLC software.