CAREER: Static-Analysis-Driven Engineering of Modern Software Systems

软件的用户都非常熟悉它的缺点：软件速度慢，软件有漏洞，软件不安全。当一个复杂的软件系统失败时，简单地指责系统的实现者无能是无益的。事实是，软件工程师在传统工程学科中处于独特的劣势，因为他们缺乏对他们设计和构建的系统的可行预测模型。也就是说，软件工程师不能像土木工程师预测桥梁在荷载作用下的行为那样预测软件在实践中的行为。这项研究的主要智力价值在于，它为软件预测科学奠定了关键的、系统的基础。更广泛的影响是使工程师能够在预测性的帮助下构建更好的软件。此外，本研究还寻求开发课程和教育材料，以培训下一代软件工程师以这种方式构建快速、安全、可靠和可靠的软件。随着这项研究转化为实践，工程师们采用这种方法，它将大大加强国家网络基础设施的基础。本研究的核心技术要点是为复杂的现代编程语言开发一种综合静态分析器的系统方法。它还探讨了该方法是否可以全部或部分自动化。为了促进该方法的发展，本研究将该方法应用于流行脚本语言（如JavaScript， Perl， PHP， Ruby和Python）的内蕴静态分析器的合成。其中许多恰好是支持现代基于网络的软件的语言。本研究的基本技术概念是将小步解释器系统地转化为静态分析器。与传统技术相比，小步分析仪具有独特的优势，包括更多优化速度和精度的机会，以及更清晰、更容易地推断分析结果的合理性。

Users of software are all too familiar with its shortcomings: softwareis slow, software is buggy and software is insecure. When a complexsoftware system fails, it is unhelpfully simplistic to blame theimplementors of the system as incompetent. The truth is that softwareengineers are uniquely disadvantaged among the traditional engineeringdisciplines because they lack a viable predictive model for thesystems they design and build. That is, a software engineer cannotpredict the behavior of software in practice in the same way that acivil engineer can predict the behavior of a bridge under load. Theprimary intellectual merit of this research is that it lays thecritical, systematic foundations for the science of prediction forsoftware. The broader impacts are to enable engineers to build bettersoftware with the aid of predictivity. Moreover, this research alsoseeks to develop courses and educational material to train the nextgeneration of software engineers in the art of constructing fast,safe, reliable and secure software in this fashion. As this researchtransfers into practice and engineers adopt this methodology, it willsignificantly strengthen the foundation of nationalcyberinfrastructure.The core technical thrust of this research is the development of asystematic method for the synthesis of static analyzers for complex,modern programming languages. It also explores whether or not thismethodology can be automated in whole or in part. To motivate thedevelopment of this method, this research applies the method to thesynthesis of intensional static analyzers for popular scriptinglanguages such as JavaScript, Perl, PHP, Ruby and Python?many of whichhappen to be the languages powering modern, web-based software. Thefoundational technical concept of this research is the systematictransformation of small-step interpreters into static analyzers.Small-step analyzers promise unique advantages over traditionaltechniques, including more opportunities for optimizing speed andprecision, and clearer, easier reasoning about the soundness of theresults of the analysis.