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