Research

Software

• Liquid Types: Safety Verification via Refinement Type Inference
• BLAST: A model checker for C based on Lazy (Predicate) Abstraction
• Vampyre: A proof generating decision procedure based on the Nelson-Oppen architecture

Ph.D Dissertation: Program Verification by Lazy Abstraction

Papers [DBLP] [Google Scholar]

		Refinement Types For Haskell   with Niki Vazou, Eric Seidel, Dimitris Vytiniotis and Simon Peyton-Jones   ICFP 2014:19th ACM SIGPLAN International Conference on Functional Programming
		LiquidHaskell: Experience With Refinement Types In The Real World   with Niki Vazou and Eric Seidel   Haskell 2014: ACM Haskell Symposium
		Abstract Refinement Types   with Niki Vazou and Patrick Rondon   ESOP 2013: 22nd European Symposium on Programming
		Dependent Types For JavaScript   with Ravi Chugh and David Herman   OOPSLA 2012: 31st ACM Conference on Object-Oriented Programming Systems, Languages and Applications
		CSolve: Verifying C With Liquid Types   with Patrick Rondon, Ming Kawaguchi and Alexander Bakst   CAV 2012: 24th Conference on Computer-Aided Verification
		Deterministic Parallelism via Liquid Effects   with Ming Kawaguchi, Patrick Rondon and Alexander Bakst   PLDI 2012: 34th ACM Conference on Programming Language Design and Implementation
		Verifying GPU Kernels By Test Amplification   with Alan Leung, Manish Gupta, Yuvraj Agarwal, Rajesh Gupta and Sorin Lerner   PLDI 2012: 34th ACM Conference on Programming Language Design and Implementation
		Nested Refinements: A Logic For Duck Typing   with Ravi Chugh and Patrick Rondon   POPL 2012: 39th ACM Symposium on Principles of Programming Languages
		HMC: Verifying Functional Programs With Abstract Interpreters   with Rupak Majumdar and Andrey Rybalchenko   CAV 2011: 23rd Conference on Computer-Aided Verification
		NV-Heaps: Making Persistent Objects Fast and Safe with Next-Generation, Non-Volatile Memories   with Joel Coburn, Adrian Caulfield, Ameen Akel, Laura Grupp, Rajesh Gupta and Steven Swanson   ASPLOS 2011: 16th ACM Conference on Architectural Support for Programming Languages and Operating Systems
		An Empirical Study of Privacy-Violating Information Flows in JavaScript Web Applications   with Don Jang, Sorin Lerner and Hovav Shacham   CCS 2010: 17th ACM Conference on Computer and Communications Security
		Dsolve: Safety Verification with Liquid Types   with Ming Kawaguchi and Patrick Rondon   CAV 2010: 22nd Conference on Computer-Aided Verification
		Finding Latent Performance Bugs in Systems Implementations   with Charles Killian, Karthik Nagaraj, Salman Pervez, Ryan Braud and James W. Anderson   FSE 2010: 16th ACM SIGSOFT Symposium on the Foundations of Software Engineering
		Low-level Liquid Types   with Patrick Rondon and Ming Kawaguchi   POPL 2010: 37th ACM Symposium on Principles of Programming Languages
		Software Model Checking   with Rupak Majumdar   ACM Computing Surveys
		Type-based Data Structure Verification   with Ming Kawaguchi and Patrick Rondon   PLDI 2009 : 31st ACM Conference on Programming Language Design and Implementation
		Staged Information Flow for JavaScript   with Ravi Chugh, Jeff Meister and Sorin Lerner   PLDI 2009 : 31st ACM Conference on Programming Language Design and Implementation
		Verifying Reference Counting Implementations   with Michael Emmi, Eddie Kohler and Rupak Majumdar   TACAS 2009: 15th Conference on Tools and Algorithms for the Construction and Analysis of Systems
		Deep Typechecking and Refactoring   with Zach Tatlock, Chris Tucker, David Shuffelton and Sorin Lerner   OOPSLA 2008: 23rd ACM Conference on Object-Oriented Programming Systems, Languages and Applications
		Liquid Types   with Patrick Rondon and Ming Kawaguchi   PLDI 2008 : 30th ACM Conference on Programming Language Design and Implementation
		Dataflow Analysis for Concurrent Programs using Datarace Detection   with Ravi Chugh, Jan Voung, and Sorin Lerner   PLDI 2008 : 30th ACM Conference on Programming Language Design and Implementation
		RELAY: Static Race Detection on Millions of Lines of Code   with Jan Voung and Sorin Lerner   FSE 2007 : 15th ACM SIGSOFT Symposium on the Foundations of Software Engineering
		Array Abstractions from Proofs   with Kenneth L. McMillan   CAV 2007 : 19th Conference on Computer-Aided Verification
		Mace: Language Support for Building Distributed Systems   with Charles Killian, James Anderson, Ryan Braud and Amin Vahdat   PLDI 2007 : 29th ACM Conference on Programming Language Design and Implementation
		Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code   with Charles Killian, James Anderson and Amin Vahdat   NSDI 2007 : 4th USENIX Symposium on Networked Systems Design and Implementation [Best Paper]
		OPIUM: Optimum Package Intall/Uninstall Management   with Chris Tucker, David Shuffelton and Sorin Lerner   ICSE 2007 : 29th ACM/IEEE International Conference on Software Engineering
		State of the Union: Type Inference via Craig Interpolation   with Rupak Majumdar and Ru-Gang Xu   TACAS 2007: 13th Conference on Tools and Algorithms for the Construction and Analysis of Systems
		Lock Allocation   with Michael Emmi, Jeff Fischer and Rupak Majumdar   POPL 2007 : 34th ACM Symposium on Principles of Programming Languages
		Interprocedural Analysis of Asynchronous Programs   with Rupak Majumdar   POPL 2007 : 34th ACM Symposium on Principles of Programming Languages
		Bit-Level Types for High-Level Reasoning   with Rupak Majumdar   FSE 2006 : 14th ACM SIGSOFT Symposium on the Foundations of Software Engineering.
		Structural Invariants   with Rupak Majumdar and Ru-Gang Xu   SAS 2006 : 13th International Static Analysis Symposium
		A Practical and Complete Approach to Predicate Refinement   with Kenneth L. McMillan   TACAS 2006 : 12th Conference on Tools and Algorithms for the Construction and Analysis of Systems
		Permissive Interfaces   with Thomas A. Henzinger and Rupak Majumdar   FSE 2005 : Symposium on the Foundations of Software Engineering
		Joining Dataflow with Predicates   with Jeffrey Fischer and Rupak Majumdar   FSE 2005 : Symposium on the Foundations of Software Engineering
		Counterexample-Guided Planning   with Krishnendu Chatterjee, Thomas A. Henzinger and Rupak Majumdar   UAI 2005 : 21st Conference on Uncertainty in Artificial Intelligence
		Interpolant-based Transition Relation Approximation   with Kenneth L. McMillan   CAV 2005 : 17th Conference on Computer-Aided Verification
		Path Slicing   with Rupak Majumdar   PLDI 2005 : 27th ACM Conference on Programming Language Design and Implementation
		Race Checking by Context Inference   with Thomas A. Henzinger, Rupak Majumdar   PLDI 2004 : 26th ACM Conference on Programming Language Design and Implementation
		Generating Tests from Counterexamples   with D. Beyer, A. Chlipala, Thomas A. Henzinger, Rupak Majumdar   ICSE 2004 : 26th ACM/IEEE International Conference on Software Engineering
		Abstractions from Proofs   with Thomas A. Henzinger, Rupak Majumdar, Kenneth L. McMillan   POPL 2004 : 31st ACM Symposium on Principles of Programming Languages
		Thread-Modular Abstraction Refinement   with Thomas A. Henzinger, Rupak Majumdar, Shaz Qadeer   CAV 2003 : 15th Conference on Computer-Aided Verification
		Counterexample-Guided Control   with Thomas A. Henzinger, Rupak Majumdar   ICALP 2003 : 30th International Colloquium on Automata, Languages and Programming
		Extreme Model Checking   with Thomas A. Henzinger, Rupak Majumdar, Marco Sanvido   International Symposium on Verification: Theory and Practice ([Invited])
		Software Verification with BLAST   with Thomas A. Henzinger, Rupak Majumdar, Gregoire Sutre   SPIN 2003 : 10th International Workshop on Model Checking Software
		Temporal-safety Proofs for Systems Code   with Thomas A. Henzinger, Rupak Majumdar, George Necula, Westley Weimer, Gregoire Sutre   CAV 2002 : 14th Conference on Computer-Aided Verification
		Lazy Abstraction   with Thomas A. Henzinger, Rupak Majumdar, Gregoire Sutre   POPL 2002 : 29th ACM Symposium on Principles of Programming Languages
		Compositional Methods for Probabilistic Systems   with Luca de Alfaro, Thomas A. Henzinger   CONCUR 2001 : 12th Conference on Concurrency Theory
		Microarchitecture Verification by Compositional Model Checking   with Kenneth L. McMillan   CAV 2001 : 13th Conference on Computer-Aided Verification

Selected Talks

• Finding Liveness Bugs in Distributed Systems
• Algorithmic Software Verification
• Type-based Data Structure Verification
• Liquid Types PPT07
• Abstractions from Proofs (Dec 2007) PPT07
• Three lectures on Lazy Abstraction (July 2005): Condensed Lecture 1 Lecture 2 Lecture 3
• Array Abstractions From Proofs (CAV '07) PPT03
• Interprocedural Analysis of Asynchronous Programs (POPL '07)
• Bit-level Types for High-level Reasoning (FSE '06)
• Tutorial: Software Verification with BLAST (SPIN '05)
• Permissive Interfaces (FSE '05)
• Race Checking by Context Inference (PLDI '04)
• Abstractions from Proofs (POPL '04)
• Thread-modular Abstraction Refinement (CAV '03)
• Temporal-safety Proofs for Systems Code (CAV '02)
• Lazy Abstraction (POPL '02)
• Compositional Methods for Probabilistic Systems (CONCUR '01)
• Microarchitectural Verification by Compositional Model Checking (CAV '01)