Correctness And Progress Verification Of Non-Blocking Programs