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

SHF：媒介：协作研究：程序分析：使用跟踪数据进行本地化、解释和综合

• 批准号: 1763814
• 负责人: Ranjit Jhala
• 金额: $ 90万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-06-15 至 2023-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1763814&HistoricalAwards=false
• 关键词: SHF; Medium; Collaborative; Research; Program

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.

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