Osbert Bastani

Osbert Bastani

Postdoctoral Researcher
Massachusetts Institute of Technology


I am currently a postdoc at MIT working with Armando Solar-Lezama. Starting in Fall 2018, I will be a research assistant professor at the Department of Computer and Information Science at the University of Pennsylvania. Previously, I (mostly) completed my Ph.D. at Stanford advised by Alex Aiken.


I am interested in techniques for developing correct software systems, including software verification and program synthesis. I am particularly excited about approaches for reasoning about machine learning algorithms, which are increasingly used in real world systems where failures can be catastrophic, for example, autonomous vehicles, medical diagnosis, and legal decision making. For such applications, there are many desirable correctness properties that machine learning algorithms should satisfy, including fairness, causality, and robustness. My work aims to address the following challenges:

  • What are useful notions of correctness for machine learning algorithms?
  • How can we reason about the correctness of existing machine learning algorithms?
  • Can we design new machine learning algorithms that are inherently correct?


Osbert Bastani, Carolyn Kim, Hamsa Bastani. Interpreting Blackbox Models via Model Extraction. In submission. [arXiv]

Osbert Bastani, Carolyn Kim, Hamsa Bastani. Interpretability via Model Extraction. FAT/ML Workshop 2017. [paper] [arxiv]

Osbert Bastani, Rahul Sharma, Alex Aiken, Percy Liang. Synthesizing Program Input Grammars. PLDI 2017. [paper] [extended] [arXiv] [code] [presentation]

Yu Feng, Osbert Bastani, Ruben Martins, Isil Dillig, Saswat Anand. Automated Synthesis of Semantic Malware Signatures using Maximum Satisfiability. NDSS 2017. [paper] [arXiv]

Osbert Bastani, Yani Ioannou, Leonidas Lampropoulos, Dimitrios Vytiniotis, Aditya Nori, Antonio Criminisi. Measuring Neural Net Robustness with Constraints. NIPS 2016. [paper] [arXiv] [poster]

Lazaro Clapp, Osbert Bastani, Saswat Anand, Alex Aiken. Minimizing GUI Event Traces. FSE 2016. [paper]

Osbert Bastani, Saswat Anand, Alex Aiken. An interactive approach to mobile app verification. MobileDeLi Workshop 2015 (Invited Paper). [paper]

Osbert Bastani, Saswat Anand, Alex Aiken. Interactively verifying absence of explicit information flows in Android apps. OOPSLA 2015. [paper]

Osbert Bastani, Saswat Anand, Alex Aiken. Specification inference using context-free reachability. POPL 2015. [paper] [presentation]

Osbert Bastani, Christopher Hillar, Dimitar Popov, Maurice Rojas. Randomization, sums of squares, near-circuits, and faster real root counting. Contemporary Mathematics 556 (2011): 145-166. [paper]