SHF: Medium: Collaborative Research: Program Analytics: Using Trace Data for Localization, Explanation and Synthesis

正式的程序分析长期以来一直承诺降低创建、维护和发展程序的成本。然而，许多关键的分析任务，如定位错误来源或建议代码修复，本质上是模棱两可的：没有唯一的正确答案。这种模棱两可的做法从根本上限制了正式工具的广泛采用，因为它将用户限制在那些具有足够专业知识、能够有效使用这种模棱两可的结果的人身上。关键的洞察是，数据驱动的机器学习方法可以应用于程序员在执行开发任务时生成的数据跟踪，这种方法在其他领域已被证明是成功的。这项研究通过将经典程序分析扩展到现代程序分析来应对歧义的挑战。这种扩展将传统的符号方法与现代数据驱动方法结合起来，共同学习程序员与编译器或分析工具交互的细粒度痕迹，以迭代地修改和修复软件。该研究通过从语言领域和编程任务两个维度进行研究，系统地发展了程序分析。首先，它研究了不同的语言领域，从动态类型语言(Python)，到带有契约系统的静态类型函数式语言(Haskell)，再到交互式证明助手(CoQ)。其次，它针对不同的编程任务，从本地化错误(如空解引用、断言或其他动态类型故障)到静态类型错误，再到完成或修复代码以消除错误或获得某些所需的功能。这种方法利用了一套新的方法，这些方法利用了最新的统计机器学习和细粒度的、特定于领域的程序员交互。这些优点使得研究能够解决经典程序分析中的歧义这一根本问题。这有可能通过产生高效、适用和可自动定制的新一代程序分析工具来改变软件开发。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Formal program analyses have long held out the promise of lowering the cost ofcreating, maintaining and evolving programs. However, many crucial analysistasks, such as localizing the sources of errors or suggesting code repairs, areinherently ambiguous: there is no unique right answer. This ambiguityfundamentally restricts the wider adoption of formal tools by limiting users tothose with enough expertise to effectively use such ambiguous results. The keyinsight is that data-driven machine-learning approaches, which have provedsuccessful in other domains, can be applied to the data traces generated byprogrammers as they carry out development tasks. This research addresses thechallenge of ambiguity by extending classical program analysis into modernprogram analytics. This extension enhances classical symbolic methods withmodern data-driven approaches to collectively learn from fine-grained traces ofprogrammers interacting with compilers or analysis tools to iteratively modifyand fix software.The research systematically develops program analytics by pursuing researchalong two dimensions: language domains and programming tasks. First, it studiesdifferent language domains, from dynamically typed languages (Python), tostatically typed functional languages with contract systems (Haskell), tointeractive proof assistants (Coq). Second, it targets different programmingtasks, from localizing errors like null-dereferences, assertions or otherdynamic type failures, to static type errors, to completing or fixing code toeliminate an error or to obtain some desired functionality. This approach takesadvantage of a suite of new approaches that harness recent advances instatistical machine learning and fine-grained, domain specific programmerinteractions. These advantages allow the research to address the fundamentalproblem of ambiguity in classical program analysis. This has potential totransform software development by yielding a new generation of program analysistools that are efficient, applicable, and automatically customizable (e.g., to aparticular company, project, group or even individual).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.