|
In recent years, model checking has gained wide acceptance as a powerful tool for hardware design and has become an integral part of the verification process in IBM and other companies. Recently, there has been increasing interest in the application of model checking to software. One approach is to develop new techniques that are specialized for software. A second approach is to use modeling techniques that allow the application of existing tools. The advantage of the former is that it allows the difficulties inherent in software model checking to be addressed directly, while the advantage of the latter is that it utilizes years of development and optimization effort put into an existing tool.
For the past few years, the IBM Haifa Research Laboratory has been pursuing the application of RuleBase to model checking of software, with the goal of eventually releasing a dedicated software model checker based on the same underlying technology. The following papers describe first steps in this direction.
| 
