Future Reasoning
Aws Albarghouthi
March 2018
We are rushing headlong into a future where every inch of our world is swallowed by complex software. It is thus imperative that we be able to reason about sophisticated program behavior and construct well-behaved programs. E.g.: My research focuses on designing next-generation program verification and synthesis technologies to answer the above questions as well as others.

Fairness in algorithmic decision-making

More and more of our critical decisions are being delegated to software. With the range and sensitivity of algorithmic decisions expanding by the day, the question of whether an algorithm is fair is a pressing one. Consider, for instance, unfairness in job applications, welfare allocation, loans, etc. The possibilities for discrimination are only expanding, and, in the near future, we might even be talking about bias and discrimination in robots interacting with humans. In the FairSquare project, we are exploring algorithmic techniques for (a) verifying fairness of decision-making programs, (b) synthesizing fair programs, and (c) automatically explaining behavior of decision-making programs.

Privacy-preserving algorithms

Data is the new oil, and data mining is a threat to individual privacy. To ensure that an individual's details are not leaked through data analysis, differential privacy has emerged as a popular formulation of privacy where random noise is added to analysis results. Differentially private algorithms have been implemented by the US Census Bureau, Apple, Google, Uber, amongst others. In this project, we are advancing verification and synthesis technology to (a) verify correctness of differentially-private algorithms, (b) verify the accuracy of these algorithms, and, ultimately, (c) synthesize them automatically.

Program synthesis for data analysis

Over the past decade, we have witnessed a transformational rise in distributed computing platforms that allowed us to seamlessly harness the power of cloud computing infrastructure for large-scale data analysis. In the BIGλ project, we are asking whether we can democratize cloud computing infrastructure, such that end users with no programming skills can use it. To do so, we are exploring how to automatically synthesize data-analysis programs from simple examples. Our work has been exploring MapReduce programs, Datalog programs, and recently we have started exploring synthesis in the context of differential privacy constraints—as described above.

Human–robot interactions

In the near future, it is highly likely that robotic agents will transform our world, be it in the workplace, in public spaces, or at home. How can we program robots to seamlessly blend into our environment? In this forward-looking project, we are developing programming technologies (languages, analyzers, and IDEs) that are aware of social norms. Picture a designer programming a human–robot interaction; the IDE would interactively inform them of potential violations of social norms, e.g., the robot coming too close to a human's personal space, or the robot rudely interrupting the human, etc. This way, designers are more aware of the impact of their designs in the environment and can tailor them to be more socially aware. The cross-cutting project connects verification technology with research in human–computer interaction and psychology.

Deep-learning-augmented development

The rise of deep learning has inspired the use of machine learning in an ever-expanding range of tasks. In this project, we are using deep learning to rethink various programming technologies. For example, we have been exploring the use of deep learning to improve the precision of static program analyses, as well as to automatically synthesize programs from natural-language descriptions.