An underlying assumption for N-version programming technique is that independently developed versions would fail in a statistically independent mannel: Howevel; empirical studies have demonstrated that common modefailures can occur even for independently developed versions, and that common modefailures degrade system reliability. In thispapel; we demonstrate that the weakestpreconditionanalysis is effective indetermining input spaces leading to commonmodefailures. Weapplied the weakestprecondition to the LaunchInterceptor Programs which were used in several otherexperiments related to the N-versionprogramming technique. We detected 13 out of 18fault pairs which have been known to cause common mode failure. These faults were due to logicaljawsinprogramdesign. 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 imp...