Osbert Bastani

Osbert Bastani

Research Assistant Professor
University of Pennsylvania


Starting in Summer 2018, I will be a research assistant professor at the Department of Computer and Information Science at the University of Pennsylvania. Currently, I am a postdoc at MIT working with Armando Solar-Lezama. Previously, I 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, Lazaro Clapp, Saswat Anand, Rahul Sharma, Alex Aiken. Eventually Sound Points-To Analysis with Missing Code. In submission. [arXiv]

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

Osbert Bastani, Rahul Sharma, Alex Aiken, Percy Liang. Active Learning of Points-To Specifications. To appear, PLDI 2018. [arXiv]

Yu Feng, Ruben Martins, Osbert Bastani, Isil Dillig. Program Synthesis using Conflict-Driven Learning. To appear, PLDI 2018. [arXiv]

Osbert Bastani. Beyond Deductive Inference in Program Analysis. Ph.D. Thesis. [thesis]

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

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] [code] [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] [presentation]

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]