{"references": ["IEC 61131-3:2003 Programmable controllers \u2013 Part 3: Programming languages, IEC Std., 2003.", "B. Fern\u00e1ndez et al., \u201cApplying model checking to industrial-sized PLC programs,\u201d IEEE Transactions on Industrial Informatics, vol. 11, no. 6, pp. 1400\u20131410, 2015.", "D. Darvas, B. Fern\u00e1ndez, and E. Blanco, \u201cPLCverif: A tool to verify PLC programs based on model checking techniques,\u201d in Proc. of the 15th Int. Conf. on Accelerator & Large Experimental Physics Control Systems, 2015.", "B. Fern\u00e1ndez, D. Darvas, J.-C. Tournier, E. Blanco, and V. M. Gonz\u00e1lez, \u201cBringing automated model checking to PLC program development \u2013 A CERN case study,\u201d in Proc. of the 12th Int. Workshop on Discrete Event Systems. IFAC, 2014, pp. 394\u2013399.", "J. Sadolewski, \u201cConversion of ST control programs to ANSI C for verification purposes,\u201d e-Informatica, vol. 5, no. 1, pp. 65\u201376, 2011.", "J. Sadolewski, \u201cAutomated conversion of ST control programs to Why for verification purposes,\u201d in Proc. of the Federated Conf. on Computer Science and Information Systems. IEEE, 2011, pp. 849\u2013854.", "A. S\u00fclflow and R. Drechsler, \u201cVerification of PLC programs using formal proof techniques,\u201d in Formal Methods for Automation and Safety in Railway and Automotive Systems. L\u2019Harmattan, 2008, pp. 43\u201350.", "N. Bauer, R. Huuck, B. Lukoschus, and S. Engell, \u201cA unifying semantics for sequential function charts,\u201d in Integration of Software Specification Techniques for Applications in Engineering, ser. Lecture Notes in Computer Science. Springer, 2004, vol. 3147, pp. 400\u2013418.", "C. B\u00f6hm and G. Jacopini, \u201cFlow diagrams, Turing machines and languages with only two formation rules,\u201d Communications of the ACM, vol. 9, no. 5, pp. 366\u2013371, 1966.", "M. de Sousa, \u201cProposed corrections to the IEC 61131-3 standard,\u201d Computer Standards & Interfaces, vol. 32, no. 5-6, pp. 312\u2013320, 2010.", "Siemens, \u201cStandards compliance according to IEC 61131-3,\u201d 2011, http://support.automation.siemens.com/WW/view/en/50204938.", "Siemens, SIMATIC Ladder Logic (LAD) for S7-300 and S7-400 Programming, 1996, C79000-G7076-C504-02."]}

Programmable Logic Controllers are typically programmed in one of the five languages defined in the IEC 61131 standard. While the ability to choose the appropriate language for each program unit may be an advantage for the developers, it poses a serious challenge to verification methods. In this paper we analyse and compare these languages to show that the ST programming language can efficiently and conveniently represent all PLC languages for formal verification purposes.