Luo, C., Qin, S., Qiu, Z., "Verifying BPEL-like Programs with Hoare Logic", Frontiers of Computer Science in China, 2008