Rudolf Berghammer, Peter Höfner, Insa Stucke: Automated Verification of Relational While-Programs. RAMiCS 2014: 173-190