SAT-based abstraction refinement for programmable logic controllers

This paper studies the application of counterexample-guided abstraction refinement to programs written in Instruction List as part of a model checking framework. More importantly, it presents an approach for automatic abstraction refinement based on SAT solving. This technique is based on an encoding of the semantics of Instruction List in propositional Boolean logic. Since elegant ideas and careful engineering have advanced SAT solvers to the state they can rapidly decide satisfiability of structured problems that involve thousands of variables, this approach scales well in practice. The true force of this method, however, is that a single description of the semantics of a program can be used to perform abstraction refinement in a number of abstract domains, including but not limited to intervals and bit sets, thereby decoupling the refinement from the chosen abstraction.