EAGER: CCF: SHF: Scalable Software Verification through Automated Derivation of Domain-Specific Optimization Tactics

社会对软件密集型系统日益增长的依赖推动了对增加软件可靠性的持续需求，使其比以往任何时候都更加重要。形式验证技术提供了最高程度的软件保证，其优势在于其自动化但严格的分析能力。然而，执行这样的形式化分析是一项昂贵的工作，面临着可伸缩性问题。当考虑到复杂系统的进化性质时，这一挑战就会加剧。因此，对于快速发展的大规模系统来说，正式验证的高成本是令人望而却步的，尽管它可以提供可靠性、安全性和安全性方面的好处。本研究旨在开发自动化软件验证技术优化开发的技术，目的是每个感兴趣的系统都可以根据其特定特征进行验证，从而显著降低验证成本。反过来，这允许软件工程师持续地在线分析不断发展的系统，而不是在整个开发过程中执行一次昂贵的、长时间运行的形式化分析。除了研究生，这个项目还将尝试让本科生、女性和少数族裔学生参与进来。这个研究项目探索了驱动软件验证技术领域特定优化的自动发现的可能性。从历史上看，这样的优化是从世界范围内几十位软件验证专家的见解中产生的。这项研究采用了一种不同的方法。该项目寻求自动推断特定于领域的、合理的优化，以削减验证范围，而不需要分析仪的任何先前的领域专业知识，承诺使软件验证显着更具可扩展性和成本效益。这项研究的智力价值是一种新颖的、推测性的分析，以已建立的、经过验证的模型发现技术为基础，自动识别推导声音优化的机会，不需要领域的专业知识或过多的开销，从而大大降低了分析成本。这项研究承诺通过使有界的形式化验证更易于处理来推进最先进的技术，从而扩大可以从形式化验证技术中实际受益的领域。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The ever-growing reliance of society on software-intensive systems drives a continued demand for increased software dependability, making it more important than ever. Formal-verification techniques provide the highest degree of software assurance, with their strengths residing in their automated yet rigorous analysis capabilities. Performing such formal analyses is, however, an expensive endeavor, facing scalability issues. This challenge is exacerbated when considering the evolving nature of complex systems. The high cost of formal verification is thus prohibitive for rapidly evolving large-scale systems, despite the benefits it can offer for reliability, safety, and security. This research seeks to develop techniques for automating the development of optimizations for software-verification techniques with the aim that each system of interest can have verification tailored to its specific characteristics, thereby significantly reducing the verification cost. This, in turn, allows software engineers to continuously analyze evolving systems online, rather than the current practice of performing expensive, long-running formal analysis once, if at all, during the entire development process. In addition to graduate students, this project will attempt to involve undergraduate, female, and underrepresented minority students.This research project explores the possibility of driving the automated discovery of domain-specific optimizations for software-verification techniques. Historically, such optimizations have arisen from the insights of a few dozen experts in software verification worldwide. This research is taking a different approach. The project seeks to automatically infer domain-specific, sound optimizations to trim the verification bounds without requiring any prior domain expertise on the part of the analyzer, promising to make software verification significantly more scalable and cost-effective. The intellectual merit of this research is a novel, speculative analysis, underpinned by established, proven model-finding technologies to automatically recognize opportunities for the derivation of sound optimizations, without requiring domain expertise or excessive overhead, thereby significantly diminishing the analysis cost. This research promises to advance the state-of-the-art by rendering bounded formal verification more tractable, thereby expanding the areas that can practically benefit from formal verification techniques.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.