Ganna Monakova, Oliver Kopp, Frank Leymann, Simon Moser, Klaus Schäfers: Verifying Business Rules Using an SMT Solver for BPEL Processes. BPSC 2009: 81-94