GPUexplore is a tool that exploits the computational power of graphics processors to efficiently construct state spaces, and on-the-fly check safety and liveness properties. Its current main practical limitation, though, is related to its input language. The tool accepts networks of Labelled Transition Systems, which were initially useful to test whether state space could be constructed efficiently on a GPU, but when one wishes to encode data variables in such an input model, the model quickly becomes unwieldy. In this talk, I will present my recent results on extending GPUexplore to support state machine models with data variables. To make this feasible, a code generator has been created that given a model, produces GPU code to interpret it. Furthermore, to make the approach practical, states are stored as binary trees to allow for sharing, and Cleary table style compression is applied to more effectively use the GPU memory. The result is that state spaces consisting of billions of states can be explored in tens of seconds. This is the first work that investigates state sharing and compression for GPUs.