This work analyzes the application of symbolic execution for state machine extraction of safety-relevant applications implemented in IEC 61131-3 with respect to the PLCopen safety standard. The theory behind symbolic execution in the given context is outlined. Furthermore, an implementation is provided and described in detail. Lastly, the capabilities of the implementation are illustrated on an example of reasonable size.