Automatic Property Checking for Software: Past, Present and Future

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 specific kind of errors more thoroughly inside the program by analyzing how control and data flow 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.