Static analysis complements software testing as an approach to assuring correctness of software. Model checking is a static analysis technique that is particularly beneficial for checking for important properties of concurrent software, such as freedom from deadlock and freedom from race conditions. A weakness of model checking is that properties are being proved of a model of the software, not the software itself. Whether those properties still hold on the software depends on how accurately the model captures the portions of the software related to the properties of interest.
In this talk, I will describe software model checking and examine an implementation technique that relies on state machines embedded within the code. I will argue that this implementation technique makes it much easier to extract an accurate model of the software for analysis, thereby increasing the value of the model checking results. I will also discuss the results of applying model checking to a non-trivial piece of software constructed in this manner, the intepreter for the Little-JIL process programming language.