About

I study the art and science of program verification and synthesis. I am a member of the madPL group, a world-class group of faculty and students at the forefront of programming languages, verification, and software engineering research.

I joined UW–Madison in 2015, after receiving my PhD at the University of Toronto, where I was advised by Marsha Chechik.

News

1/19Our Datalog engine paper to appear at VLDB!
11/18 Paper on synthesis with equivalence reduction to appear at VMCAI
10/18 Paper on fairness-aware programming to appear at FAT*
10/18 Paper on verifying accuracy of randomized algorithms to appear at POPL
10/18 Best paper award at UIST! Way to go, David!
7/18 Paper on verification for human-robot interactions accepted to UIST!
6/18 Paper on type-directed enocders and static analysis accepted to FSE!
6/18 Paper on Datalog synthesis with active learning accepted to FSE!
3/18 Paper on synthesizing probabilistic proofs accepted to CAV!
3/18 Excited to be giving a keynote at FairWare@ICSE in Sweden!
2/18 Baby Lea Maria arrives in our world!
2/18 Excited to be serving on the POPL19 PC!
2/18 Best paper award at FAST!
2/18 Excited to be giving an invited talk at SAS in Freiburg!

Research

See my research agenda for details on my current work; below, you find short descriptions of two of my main projects. I am always looking for ambitious PhD and undergraduate students. If you're interested in working with me, email me.

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

The FairSquare project develops new probabilistic verification and synthesis techniques for fairness in decision-making programs.
Papers FATML16, CAV17, IJCAI17, SAS17, OOPSLA17, POPL18
Media NBC, Daily Texan, Wisconsin State Journal, Engadget, TechRepublic

Papers

Scaling-Up In-Memory Datalog Processing
Zhiwei Fan, Jianqiao Zhu, Zuyu Zhang, Aws Albarghouthi, Paraschos Koutris, Jignesh Patel
VLDB 19 Very Large Databases

Fairness-Aware Programming
Aws Albarghouthi, Samuel Vinitsky
FAT* 19 Fairness, Accountability, and Transparency

Trace Abstraction Modulo Probability
Calvin Smith, Justin Hsu, Aws Albarghouthi
POPL 19 Principles of Programming Languages

Program Synthesis with Equivalence Reduction
Calvin Smith, Aws Albarghouthi
VMCAI 19 Verification, Model Checking, and Abstract Interpretation

Fairness: A Formal-Methods Perspective
Aws Albarghouthi
SAS 18 Static Analysis
Paper accompanying invited talk

Authoring and Verifying Human–Robot Interactions
David Porfirio, Allison Sauppé, Aws Albarghouthi, Bilge Mutlu
UIST 18 User Interface Software and Technology
🏆 Best paper award

Neural-Augmented Static Analysis of Android Communication
Jinman Zhao, Aws Albarghouthi, Vaibhav Rastogi, Somesh Jha, Damien Octeau
FSE 18 Foundations of Software Engineering

Syntax-Guided Synthesis of Datalog Programs
Xujie Si, Woosuk Lee, Richard Zhang, Aws Albarghouthi, Paris Koutris, Mayur Naik
FSE 18 Foundations of Software Engineering

Constraint-Based Synthesis of Coupling Proofs
Aws Albarghouthi and Justin Hsu
CAV 18 Computer Aided Verification

Synthesizing Coupling Proofs of Differential Privacy
Aws Albarghouthi and Justin Hsu
POPL 18 Principles of Programming Languages

Distribution Policies for Datalog
Bas Ketsman, Aws Albarghouthi and Paraschos Koutris
ICDT 18 Database Theory

Protocol-Aware Recovery for Consensus-Based Storage
Ramnatthan Alagappan, Aishwarya Ganesan, Vijay Chidambaram, Aws Albarghouthi, Andrea Arpaci-Dusseau, Remzi Arpaci-Dusseau
FAST 18 File and Storage Technologies
🏆 Best paper award

FairSquare: Probabilistic Verification for Program Fairness
Aws Albarghouthi, Loris D'Antoni, Samuel Drews, Aditya Nori
OOPSLA 17 OO Programming, Systems, Languages, and Applications

Discovering Relational Specifications
Calvin Smith, Gabriel Ferns, Aws Albarghouthi
FSE 17 Foundations of Software Engineering
🏆 Best paper award

Probabilistic Horn Clause Verification
Aws Albarghouthi
SAS 17 Static Analysis

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

Constraint-Based Synthesis of Datalog Programs
Aws Albarghouthi, Paris Koutris, Mayur Naik, Calvin Smith
CP 17 Constraint Programming

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

Fairness as a Program Property
Aws Albarghouthi, Loris D'Antoni, Samuel Drews, 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, 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, Remzi Arpaci-Dusseau
HotOS 15 Hot Topics in Operating Systems

Spatial Interpolants
Aws Albarghouthi, Josh Berdine, Byron Cook, 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, 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, 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, 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, Marsha Chechik
CAV 12 Computer Aided Verification

From Under-approximations to Over-approximations and Back
Aws Albarghouthi, Arie Gurfinkel, 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, Marsha Chechik
VMCAI 12 Verification, Model Checking, and Abstract Interpretation

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

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

On the Use of Planning Technology for Verification
Aws Albarghouthi, Jorge A. Baier, 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

S19 CS 704: Principles of Programming Languages
F18 CS 536: Intro to Compilers and Proramming Languages
S18 CS 704: Principles of Programming Languages
F17 CS 536: Intro to Compilers and Programming Languages
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

19 POPL, FAT* (track co-chair), CAV, VSTTE
18 FAT*, CAV, ICSE Doctoral Symposium, SMT, ATVA
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