Symbolic model verifier (SMV), an automatic error finding system, is developed and applied to various chemical processing systems to test their safety and feasibility. In this paper, we adopted SMV to synthesize error-free operating schedules in multi-purpose batch processes. The strength of this method is to synthesize a feasible sequence and to verify its safety simultaneously. Here, we propose two algorithms. One is to find embedded errors in operating sequences such as violating intermediate storage tank policies and unavailability due to sudden operating condition changes or insufficient production recipes. The other is the completion time algorithm to make sure that a makespan and a final operating sequence are obtained without errors. The proposed algorithm identifies errors and finds a minimum makespan and an operating sequence. Computation tree logic (CTL) embedded in SMV is extensively used to describe the situation of unsafe conditions and time related conditions for the final makespan. As a result of applying the algorithms to multi-purpose chemical processes, this approach finds a makespan and error-free operating schedules successfully. This combined synthesis and verification method also reduces the computation time and verifies operating schedules efficiently compared with the previously published algorithms.