An underlying assumption for N-version programming technique is that independently developed versions would fail in a statistically independent manner. However, empirical studies have demonstrated that common mode failures can occur even for independently developed versions, and that common mode failures degrade system reliability. In this paper, we demonstrate that the weakest precondition analysis is effective in determining input spaces leading to common mode failures. We applied the weakest precondition to the Launch Interceptor Programs which were used in several other experiments related to the N-version programming technique. We detected 13 out of 18 fault pairs which have been known to cause common mode failure. These faults were due to logical flaws in program design. Although the weakest precondition analysis may be labor-intensive since they are applied manually, our results convincingly demonstrate that it is effective for identifying input spaces causing common mode failures and further improving the reliability of N-version software.