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

University Of California-San Diego, La Jolla CA

Investigators

Abstract

Formal program analyses have long held out the promise of lowering the cost of creating, maintaining and evolving programs. However, many crucial analysis tasks, such as localizing the sources of errors or suggesting code repairs, are inherently ambiguous: there is no unique right answer. This ambiguity fundamentally restricts the wider adoption of formal tools by limiting users to those with enough expertise to effectively use such ambiguous results. The key insight is that data-driven machine-learning approaches, which have proved successful in other domains, can be applied to the data traces generated by programmers as they carry out development tasks. This research addresses the challenge of ambiguity by extending classical program analysis into modern program analytics. This extension enhances classical symbolic methods with modern data-driven approaches to collectively learn from fine-grained traces of programmers interacting with compilers or analysis tools to iteratively modify and fix software. The research systematically develops program analytics by pursuing research along two dimensions: language domains and programming tasks. First, it studies different language domains, from dynamically typed languages (Python), to statically typed functional languages with contract systems (Haskell), to interactive proof assistants (Coq). Second, it targets different programming tasks, from localizing errors like null-dereferences, assertions or other dynamic type failures, to static type errors, to completing or fixing code to eliminate an error or to obtain some desired functionality. This approach takes advantage of a suite of new approaches that harness recent advances in statistical machine learning and fine-grained, domain specific programmer interactions. These advantages allow the research to address the fundamental problem of ambiguity in classical program analysis. This has potential to transform software development by yielding a new generation of program analysis tools that are efficient, applicable, and automatically customizable (e.g., to a particular 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.