Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code

This paper presents an efficient static analysis for programmable logic controller code. For each program line (or each function block call), the analysis calculates an over-approximation of the possible values each variable can assume during all possible executions. This information can then be used to automatically check for certain critical program conditions such as division-by-zero and array-out-of-bounds. To make this approach applicable to large programs comprising many variables, we present a technique that only stores the values of a subset of the variables based on their context and liveness. We show how to detect typical problems in real PLC code.