Predicate Pairing for program verification