Automatic Property Checking for Software: Past, Present and Future - Rajamani, Sriram (Proceedings of the 4th International Conference on Software Engineering and Formal Methods (SEFM), 2006)
Software validation is a very hard problem. Traditionally, most validation in our industry has been done by testing. Testing is the process of running software on representative inputs and checking if the software behaves as intended. There are various granularities in which testing is performed —ranging from unit tests that test small units of the system, to system-wide tests. Over the past decade, automatic property checking tools that use static analysis have started providing a complementary approach to software validation. These tools are intended to augment, rather than replace, testing. These tools do not typically ensure that the software implements intended functionality correctly. Instead, they look for speciﬁc kind of errors more thoroughly inside the program by analyzing how control and data ﬂow through the program. This short paper surveys the state of the art in property checking tools and presents the author’s personal perspective on future research in this area.