Aws Albarghouthi's Homepage

I study the art and science of program analysis, verification, and synthesis
I am a member of the madPL group
I joined the University of Wisconsin–Madison in 2015
I got my PhD at the University of Toronto, working with Marsha Chechik

NEWS

June 17 New paper at SAS17
June 17 NSF grant to work on formal methods of program fairness!
June 17 New paper by Calvin to appear at FSE17
Apr 17 New paper by David M. to appear at IJCAI17
Apr 17 New paper by Sam to appear at CAV17
Mar 17 David P. receives the NSF Graduate Research Fellowship!
Mar 17 Sam is quoted in NBC article on algorithmic bias
Feb 17 Received an NSF CAREER Award!
Jan 17 Sam lands 2nd place at POPL's student research competition

MAIN PROJECTS

BIGλ The BIGλ project develops foundational program synthesis techniques, with an emphasis on big-data programming.
Papers POPL16, PLDI16, FSE17
Funding NSF

FairSquare The FairSquare project develops new probabilistic verification and synthesis techniques for fairness in decision-making programs.

Papers

Funding

Media

NBC

Daily Texan

PAPERS

Probabilistic Horn Clause Verification
Aws Albarghouthi
SAS 17 Static Analysis Symposium

Discovering Relational Specifications
Calvin Smith, Gabriel Ferns, and Aws Albarghouthi
FSE 17 Foundations of Software Engineering

Weighted Model Integration via Orthogonal Transformations
David Merrell, Aws Albarghouthi, and Loris D'Antoni
IJCAI 17 Aritificial Intelligence

Repairing Decision-Making Programs under Uncertainty
Aws Albarghouthi, Loris D'Antoni, and Samuel Drews
CAV 17 Computer Aided Verification

Quantifying Program Bias
Aws Albarghouthi, Loris D'Antoni, Samuel Drews, and Aditya Nori
arXiv:1702.05437

Fairness as a Program Property
Aws Albarghouthi, Loris D'Antoni, Samuel Drews, and Aditya Nori
FATML 16 Fairness, Accountability, and Trasparency in Machine Learning

Effectively Propositional Interpolants
Samuel Drews and Aws Albarghouthi
CAV 16 Computer Aided Verification

MapReduce Program Synthesis
Calvin Smith and Aws Albarghouthi
PLDI 16 Programming Languages Design and Implementation

Maximal Specification Synthesis
Aws Albarghouthi, Isil Dillig, and Arie Gurfinkel
POPL 16 Principles of Programming Languages

Beyond Storage APIs: Provable Semantics for Storage Stacks
Ramnatthan Alagappan, Vijay Chidambaram, Thanumalayan Sankaranarayana Pillai,
Aws Albarghouthi, Andrea Arpaci-Dusseau, and Remzi Arpaci-Dusseau
HotOS 15 Hot Topics in Operating Systems

Spatial Interpolants
Aws Albarghouthi, Josh Berdine, Byron Cook, and Zachary Kincaid
ESOP 15 European Symposium on Programming

Software Verification with Program-Graph Interpolation and Abstraction
PhD Thesis, University of Toronto, 15

Symbolic Optimization with SMT Solvers
Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, and Marsha Chechik
POPL 14 Principles of Programming Languages

Beautiful Interpolants
Aws Albarghouthi and Ken McMillan
CAV 13 Computer Aided Verification

Recursive Program Synthesis
Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid
CAV 13 Computer Aided Verification

UFO: Verification with Interpolants and Abstract Interpretation
Aws Albarghouthi, Arie Gurfinkel, Yi Li, Sagar Chaki, and Marsha Chechik
TACAS 13 Tools and Algorithms for the Construction and Analysis of Systems
International Competition on Software Verification (SV-COMP) Contribution
UFO won 4 gold medals—the largest number of gold medals won by any tool

Parallelizing Top-down Interprocedural Analyses
Aws Albarghouthi, Rahul Kumar, Aditya Nori, and Srirarm Rajamani
PLDI 12 Programming Languages Design and Implementation

UFO: A Framework for Abstraction- and Interpolation-Based Software Verification
Aws Albarghouthi, Yi Li, Arie Gurfinkel, and Marsha Chechik
CAV 12 Computer Aided Verification

From Under-approximations to Over-approximations and Back
Aws Albarghouthi, Arie Gurfinkel, and Marsha Chechik
TACAS 12 Tools and Algorithms for the Construction and Analysis of Systems

Whale: An Interpolation-based Algorithm for Inter-procedural Verification
Aws Albarghouthi, Arie Gurfinkel, and Marsha Chechik
VMCAI 12 Verification, Model Checking, and Abstract Interpretation

Craig Interpretation
Aws Albarghouthi, Arie Gurfinkel, and Marsha Chechik
SAS 12 Static Analysis Symposium

Abstract Analysis of Symbolic Executions
Aws Albarghouthi, Arie Gurfinkel, Ou Wei, and Marsha Chechik
CAV 10 Computer Aided Verification

On the Use of Planning Technology for Verification
Aws Albarghouthi, Jorge A. Baier, and Sheila A. McIlraith
VVPS 09 Validation and Verification of Planning and Scheduling Systems

STUDENTS

Samuel Drews
David Merrell
David Porfirio
Calvin Smith
Jinman Zhao

TEACHING

S17 CS 704: Principles of Programming Languages
S16 CS 704: Principles of Programming Languages
F15 CS 536: Intro to Compilers and Programming Languages
S15 CS 704: Principles of Programming Languages

SERVICE

18 ICSE Doctoral Symposium
17 CAV, PLDI ERC, APLAS
16 CAV AEC chair, PLDI ERC, TACAS, CAV ERC, ICSE demos
15 CAV, iCAV, PLDI SRC, VMCAI
14 SV-COMP

Miscellanea
My first name rhymes with house—i.e., pronounced ouse
I have no relation to the popular cloud platform with the same name
To my knowledge, my PhD thesis (p. 77) is the first CS thesis to cite Jay Z