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

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

• 批准号: 1763674
• 负责人: Westley Weimer
• 金额: $ 30万
• 依托单位: Regents of the University of Michigan - Ann Arbor
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-06-15 至 2023-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1763674&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的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

CirFix: Automated Hardware Repair and its Real-World Applications

• DOI: 10.1109/tse.2023.3269899
• 发表时间: 2023-07
• 期刊: IEEE Transactions on Software Engineering
• 影响因子: 7.4
• 作者: Priscila Santiesteban;Yu Huang;Westley Weimer;Hammad Ahmad

CirFix: automatically repairing defects in hardware design code

• DOI: 10.1145/3503222.3507763
• 发表时间: 2022-02
• 期刊: Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems
• 作者: Hammad Ahmad;Yu Huang;Westley Weimer