This paper presents a method for model checking programs for programmable logic controllers (PLCs) using the counterexample-guided abstraction refinement (CEGAR) approach. The technique is tailored to this specific hardware platform by accounting for the cyclic scanning mode that is symptomatic to PLCs. In particular, the hardware model poses the need for on-the-fly abstraction refinement in order to guarantee a deterministic control flow. It also allows to treat refinement phases triggered by input and global variables differently, leading to a more effective implementation. The effectiveness of this approach is shown in a case study, which highlights the verification process for function blocks that implement a specification provided by the industrial consortium PLCopen.