Formal Software Analysis Emerging Trends in Software Model Checking

The study of methodologies and techniques to produce correct software has been active for four decades. During this period, researchers have developed and investigated a wide variety of approaches, but techniques based on mathematical modeling of program behavior have been a particular focus since they offer the promise of both finding errors and assuring important program properties. The past fifteen years have seen a marked and accelerating shift towards algorithmic formal reasoning about program behavior - we refer to these as formal software analysis. In this paper, we define formal software analyses as having several important properties that distinguish them from other forms of software analysis. We describe three foundational formal software analyses, but focus on the adaptation of model checking to reason about software. We review emerging trends in software model checking and identify future directions that promise to significantly improve its cost-effectiveness.