One of the important tasks during software testing is the generation of test cases. Unfortunately, existing approaches to test case generation often have problems limiting their use. A problem of dynamic test case generation approaches, for instance, is that a large number of iterations can be necessary to obtain test cases. This article introduces a formal framework for the application of the well-known search strategy of binary search in path-oriented test case generation and explains the binary search-based test case generation (BINTEST) algorithm.