Abstract

Software correctness and security have been a central issue in the field for decades. Researchers have developed a wide range of approaches to these problems, none of which has solved these problems to date.

In this talk I consider two very different approaches to solving correctness and security problems, failure-oblivious computing and domain-specific languages. I will discuss how these approaches (as well as others) interact with the cognitive limitations and available technical skills of the human population of software developers that currently must be part of any solution for it to be successful. I’ll conclude by outlining a new approach that, by deploying automated programming language technology in an appropriately targeted way, may interact more productively with the characteristics of the developer population as a whole.

Bio

Martin C. Rinard is a professor in the Department of Electrical Engineering and Computer Science at the Massachusetts Institute of Technology, and a member of the Computer Science and Artificial Intelligence Laboratory.

Dr. Rinard received the Sc.B. in Computer Science, Magna cum Laude and with Honors, from Brown University in 1984. He spent the next several years working for two startup companies, Ikan Systems and Polygen Corporation. He then entered the Ph.D. program in Computer Science at Stanford University and received the Ph.D. in Computer Science from Stanford University in 1994. He joined the Computer Science Department at the University of California, Santa Barbara as an Assistant Professor in 1994, then moved to MIT as an Assistant Professor in 1997. He was promoted to Associate Professor in 2000, Associate Professor with tenure in 2002, and Professor in 2006.

Dr. Rinard’s research focuses on software systems and related topics. The broad goal is to obtain better software - making software more robust, resilient, and secure, improving the performance, verifying that the software satisfies important correctness, acceptability, reliability, or accuracy properties, or making systems (both software and hardware) easier to specify, build, maintain, or improve. Dr. Rinard’s research results have consistently placed him at the forefront of his chosen field for decades:

• His software engineering research delivered the first use of machine learning for automatically generating correct patches for large production software systems.

• His software systems research produced numerous techniques, such as failure-oblivious computing, cyclic memory allocation, and data structure repair, that have been shown to substantially increase the robustness, reliability, and security of production software applications.

• His approximate computing research pioneered foundational techniques such as loop perforation, dynamic knobs, and implementation selection that enable programs to productively navigate complex performance versus accuracy tradeoffs.

• His program verification research produced advances such as the first full functional verification of linked data structures, the first verification of reliability and accuracy properties of approximate computations, and the first relational program logic for proving program acceptability and correctness properties involving relationships between multiple programs.

• His program analysis research produced the first pointer and escape analysis for parallel and multithreaded programs, the first sound input filters for integer overflow errors, and techniques for analyzing and transforming programs that implement divide and conquer algorithms.

• His parallel computing research pioneered the identification and exploitation of commuting operations for automatic parallelization and deterministic parallel execution.

• His computer security research produced new techniques that eliminate security vulnerabilities by automatically locating and transferring correct code across applications, by statically analyzing information flow in complex software, and by efficiently tracking provenance information in running systems. Applications of these techniques include the detection and elimination of advanced persistent threats, the identification of critical information flow properties, and the identification and nullification of information exfiltration attacks.

Dr. Rinard is an ACM Fellow and has won multiple best and distinguished paper awards at top publication venues.