Software model checking: extracting verification models form source code

摘要

To formally verify a large software application, the standard method is to invest a considerable amount of time and expertise into the manual construction of an abstract model, which is then analysed for its properties by either a mechanized or a human prover. There are two problems with this approach. The first problem is that this verification method can be no more reliable than the humans that perform the manual steps. If the average rate of error for human work is a function of the problem size, this holds not only for the construction of the original application, but also for the construction of the model.