It would obviously be very valuable to know in advance which files in the next release of a large software system are most likely to contain the largest numbers of faults. To accomplish this, we developed a negative binomial regression model and used it to predict the expected number of faults in each file of the next release of a system. The predictions are based on code characteristics and fault and modification history data. We will discuss what we have learned from applying the model to several large industrial systems, each with multiple years of field exposure, and tell you about our success in making accurate predictions and some of the lessons learned and issues that had to be dealt with.

In recent years, we see a growing awareness to the importance of assessing the quality of specifications. In the context of model checking, this can be done by analyzing the effect of applying mutations to the specification or the system. If the system satisfies the mutated specification, we know that some elements of the specification do not play a role in its satisfaction, thus the specification is satisfied in some vacuous way. If the mutated system satisfies the specification, we know that some elements of the system are not covered by the specification. Coverage in model checking have been adopted from the area of testing, where coverage information is crucial in measuring the exhaustiveness of test suites. It is now time for model checking to pay back, and let testing enjoy the rich theory and applications of vacuity. We define and study vacuous satisfaction in the context of testing, and demonstrate how vacuity analysis can lead to better specifications and test suits.

The verification market is customer led but the customers are fearful and largely not well informed. This means that any use of sophisticated methods needs to be surreptitious to quell the fear factor. The realisation that no verification technique is wholly reliable or convincing is leading to a change of thinking. The emphasis is on using complementary techniques which provide some degree of independence in verification activities. The way forward, surely, is to bring together the techniques at our disposal and on a project by project basis choose those techniques which in combination yield a cost-effective demonstration that the implemented system is the one required and that system is fault free.