Aws Albarghouthi

I am a PhD student in the Software Engineering group at the University of Toronto.
My advisor is Marsha Chechik.

My research interests lie mainly in software verification. I am particularly interested in software verification techniques that utilize Craig interpolation as a means for constructing proofs of correctness. More recently, I have started developing techniques for recursive program synthesis.

Email: aws AT cs DOT toronto DOT edu

CV (pdf)

News

• March 6 2013 Two papers accepted to CAV 2013.
• March 4 2013 I will be at Microsoft Research Cambridge for the next three months.
• Dec 16 2012: Our verifier UFO won 4 gold medals and 1 bronze medal at the International Competition on Software Verification (SV-COMP).
  Gold categories: (1) Linux Device Drivers 64-bit, (2) Control Flow and Integer variables (Windows device drivers, SSH models, etc.),
  (3) SystemC, (4) Product Lines.
  Bronze categories: Loops
• July 10 2012: The UFO software verification tool and framework is now available!

Publications

• Symba: Symbolic Abstraction with SMT Solvers
  Yi Li, Aws Albarghouthi, Arie Gurfinkel, Zachary Kincaid, and Marsha Chechik
  In submission
  
  
• Beautiful Interpolants
  Aws Albarghouthi and Ken McMillan
  CAV 2013 [Conference on Computer Aided Verification (to appear)]
  
  
• Recursive Program Synthesis
  Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid
  CAV 2013 [Conference on Computer Aided Verification (to appear)]
  
  
• UFO: Verification with Interpolants and Abstract Interpretation
  Aws Albarghouthi, Arie Gurfinkel, Yi Li, Sagar Chaki, and Marsha Chechik
  International Competition on Software Verification (SV-COMP) Contribution.
  TACAS 2013 [Conference on Tools and Algorithms for the Construction and Analysis of Systems]
  UFO won 4 gold medals and 1 bronze medal.
  
  
• Craig Interpretation
  Aws Albarghouthi, Arie Gurfinkel, and Marsha Chechik
  SAS 2012 [Static Analysis Symposium]
  
  
• UFO: A Framework for Abstraction- and Interpolation-Based Software Verification
  Aws Albarghouthi, Yi Li,, Arie Gurfinkel, and Marsha Chechik
  CAV 2012 [Conference on Computer Aided Verification]
  
  
• Parallelizing Top-down Interprocedural Analyses
  Aws Albarghouthi, Rahul Kumar, Aditya Nori, and Srirarm Rajamani
  PLDI 2012 [Conference on Programming Languages Design and Implementation]
  
  
• From Underapproximations to Overapproximations and Back
  Aws Albarghouthi, Arie Gurfinkel, and Marsha Chechik
  TACAS 2012 [Conference on Tools and Algorithms for the Construction and Analysis of Systems]
  
  
• Whale: An Interpolation-based Algorithm for Inter-procedural Verification [slides] [full version]
  Aws Albarghouthi, Arie Gurfinkel, and Marsha Chechik
  VMCAI 2012 [Conference on Verification, Model Checking, and Abstract Interpretation]
  
  
• Abstract Analysis of Symbolic Executions [slides]
  Aws Albarghouthi, Arie Gurfinkel, Ou Wei, and Marsha Chechik
  CAV 2010 [Conference on Computer-Aided Verification]
  
  
• On the Use of Planning Technology for Verification [slides]
  Aws Albarghouthi, Jorge A. Baier, and Sheila A. McIlraith
  VVPS 2009 [Workshop on Validation and Verification of Planning and Scheduling Systems]

Tools

• UFO: A tool and a framework for experimenting with interpolation-based verification,
  abstraction-based verification, as well as interesting combinations of both!
  (See our TACAS 2012 paper for details.)
  
  
• Whale: An interpolation-based interprocedural software model checker.
  Whale computes function summaries using interpolants from under-approximations of functions.
  (See our VMCAI 2012 paper for details.)
  
  
• I have been fortunate enough to work on the Yogi project
  when I interned at the Programming Languages and Tools group of Microsoft Research India in the summer of 2011.
  (See our PLDI 2012 paper for details.)

Teaching Assistantships

• CSC301 - Introduction to Software Engineering, Fall 2009
• CSC190 - Data Structures and Algorithms, Winter 2009
• CSC270 - Software Design, Fall 2008
• ENG1D04 - Engineering Computation (McMaster University), Fall 2006, Fall 2007 & Winter 2008

Contact Information

University of Toronto
Bahen Center, Room 3232
40 St. George St.
Toronto, Ontario