From a more proof-theoretic and automated deduction perspective, it was interesting to see what is researched in model checking and in SAT solvers. They seem to do more engineering oriented research, trying to have good implementations and algorithms to overcome the state space explosion when modeling always more complicated softwares; while we try to work more in expressiveness of the logic and postpone, as much as possible, to implement specific algorithms that can handle some specific cases. So there is a contrasting approach in the communities: the theorem proving employes more logicians, while the model checking community employes more engineers.
However, I was very impressed on how far the engineers/model checkers/SAT solvers can go by "hacking" logic to be efficient. They seem to have many more applications cases than the automated theorem proving community, and seem to attract more and more the attention of industries. The negative aspect is that the size of software models seems to be growing much faster than the computational power of computers, what implies that more "hacks" would be necessary to obtain efficient implementations, and with these "hacks" more mysterious these systems would be. Moreover, the properties that we would like to be proved also tend to be more expressive, and hence may not be possible to check them by using model checkers at all. Therefore, I believe that in the future there will be an increasing demand for theorem provers, and to meet this demand, we must research more logic. This does not mean, however, that model checkers will not be used any longer. I believe that for simple properties, model checkers will continue to be used in larger scale, as proving with model checkers is in general easier than with theorem provers.
No comments:
Post a Comment