Advances in Software Model Checking

Society is becoming increasingly dependent on software which results in an increasing cost of software malfunction. At the same time, software is getting increasingly complex and testing and verification are becoming harder and harder. Software model checking is a set of techniques to automatically check properties in a model of the software. The properties can be written in specialized languages or be embedded in software in the form of exceptions or assertions. The model can be explicitly provided in a specification language, can be derived from the software system, or the software system itself can be used as a model. Software model checkers check the given properties in a large number of states of the model. If a model checker is able to verify a property on all model states, it is proven that the property holds and the model checker works like a theorem prover. If a model checker is unable to verify a property on all model states, the model checker is still an efficient automated testing technique. This chapter discusses advances in software model checking and focuses on techniques that use the software as its model and embedded exceptions or assertions as the properties to be verified. Such techniques are most likely to be widespread in the software industry in the coming decade due to their minimal overhead on the programmer and due to recent advances in research making these techniques scale.