Osbert Bastani

Osbert Bastani

Ph.D. candidate in computer science
Stanford University

I am a fifth-year Ph.D. student advised by Alex Aiken.

Research Interests

As software has become pervasive in critical infrastructure, it has simultaneously become incredibly complex, making it difficult for developers to reason about correctness. Programming tools help manage this complexity by automating such reasoning. In the last few decades, a number of program analysis tools have been developed to help identify security vulnerabilities and improve software quality. However, many of these tools rely on the increasingly tenuous assumption that all relevant information is available for analysis. In real systems, there are inevitably parts of the program that are missing (e.g., dynamically loaded code) or very difficult to statically analyze (e.g., native code such as system APIs). Furthermore, the desired property may itself be too complex to specify, e.g., properties of machine learning models.

My primary research interests are developing techniques to address these challenges. In particular, my goals are to apply ideas from artificial intelligence, machine learning, and program synthesis, to (i) enable human analysts to interact with the program analysis to achieve their goals, and (ii) automatically infer program properties based on auxiliary information such as usage or execution traces. In general, I believe there is a huge opportunity for incorporating such novel inference techniques into programming tools in a way that substantially improves our ability to develop and maintain complex software.


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

Yu Feng, Osbert Bastani, Ruben Martins, Isil Dillig, Saswat Anand. Automated Synthesis of Semantic Malware Signatures using Maximum Satisfiability. To appear, 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]

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]