Deductive Verification of Parallel Programs Using Why3