It is well known that various scalability issues affect automated formal verification, and thus some approaches need to be taken to simplify the software under analysis, or the verification problem as a whole. Bounded verification is one of these approaches, that consists of checking the correctness of a program with respect to its formal specification, but limiting the number of iterations that loops may perform, as well as the maximum number of objects involved in program states.

Despite the limits imposed on the software under analysis, bounded verification still suffers from scalability issues, enabling in many cases to analyze programs only for very small scopes (the limit in the objects of program states and loop iterations). In order to further scale up bounded verification, it has been shown that by appropriately removing infeasible cases from the values that program variables (e.g., object fields) can take, bounded verification can be significantly improved. In this talk I will describe this mechanism, known as tight field bound computation, and how it can be used to contribute substantially to various program analyses, including symbolic execution and automated test input generation.