A method for automated software debugging includes steps of: receiving an interface configured for accessing a program; receiving a behavioral model of the program; receiving a failing input sequence from the program; executing the failing input sequence on both the behavioral model and the program; validating, after each executing step, an expected behavior of the program by executing specially constructed test sequences from the behavioral model; performing model mutation for creating a hypothesis of faulty behaviors; verifying hypothesized faulty behaviors; and scoring hypothesized faulty behaviors for producing a ranked list of diagnoses. The method also includes a step of presenting the ranked list of diagnoses to a user.