1. A method for inferring preconditions for procedures in a program, comprising: formulating predicates based on inputs to a procedure, including formal arguments, global variables and external environment; sampling truth assignments to the predicates to provide truth assignments that lead to a feasible set of input values; generating test cases for testing the program in accordance with the truth assignments having feasible sets of input values; and classifying the truth assignments to the predicates as providing an error or not providing an error.