Users of software are all too familiar with its shortcomings: software is slow, software is buggy and software is insecure. When a complex software system fails, it is unhelpfully simplistic to blame the implementors of the system as incompetent. The truth is that software engineers are uniquely disadvantaged among the traditional engineering disciplines because they lack a viable predictive model for the systems they design and build. That is, a software engineer cannot predict the behavior of software in practice in the same way that a civil engineer can predict the behavior of a bridge under load. The primary intellectual merit of this research is that it lays the critical, systematic foundations for the science of prediction for software. The broader impacts are to enable engineers to build better software with the aid of predictivity. Moreover, this research also seeks to develop courses and educational material to train the next generation of software engineers in the art of constructing fast, safe, reliable and secure software in this fashion. As this research transfers into practice and engineers adopt this methodology, it will significantly strengthen the foundation of national cyberinfrastructure. The core technical thrust of this research is the development of a systematic method for the synthesis of static analyzers for complex, modern programming languages. It also explores whether or not this methodology can be automated in whole or in part. To motivate the development of this method, this research applies the method to the synthesis of intensional static analyzers for popular scripting languages such as JavaScript, Perl, PHP, Ruby and Python?many of which happen to be the languages powering modern, web-based software. The foundational technical concept of this research is the systematic transformation of small-step interpreters into static analyzers. Small-step analyzers promise unique advantages over traditional techniques, including more opportunities for optimizing speed and precision, and clearer, easier reasoning about the soundness of the results of the analysis.
CAREER: Static-Analysis-Driven Engineering of Modern Software Systems