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

点击翻译按钮获取中文摘要

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.