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 research. I joined UW–Madison in 2015, after receiving my PhD at the University of Toronto, where I was advised by Marsha Chechik.

See my research agenda for an overview of my work. I'm always looking for ambitious PhD and undergrad students. Email me if you're interested.

🔥

1.21 2 new Drs in the house: Congrats to Dr. Sam Drews and Dr. Jinman Zhao!
1.21 Paper on learning privacy mechanisms to appear at S&P 21
1.21 Figaro conditionally accepted to CHI 21; congrats to David and Laura
12.20 Gave a talk at Waterloo's ML+Logic Colloqium
10.20 I'm the publicity chair for MAPL 21, a great workshop on ML and PL
10.20 Serving on the PC of AAAI, FAccT, and IJCAI
5.20 Two probability and programming research awards from FB!
5.20 Yuhao's paper on NLP robustness accepted to ICML!
5.20 Jiani and Calvin's paper on referring expressions accepted to ICML!
5.20 My first PhD student, Calvin Smith, is now a doctor!
2.20 I'm on the PC of the MAPL workshop (at PLDI). Submit your best ML/PL work!
2.20 I'm co-chairing the FoMLAS workshop in LA. Submit your best ML/FM work!
2.20 Sam's paper on data-poisoning robustness (cond.) accepted to PLDI!
12.19 David's work on adapting robot programs accepted to CHI!
11.19 Goutham + Yun Chan's paper on actionable explanations appears at AAAI!

Papers

see also preprints on arxiv / dblp

Learning Differentially Private Mechanisms
Subhajit Roy, Justin Hsu, Aws Albarghouthi
S&P 21 Security and Privacy (Oakland)

Figaro: A Tabletop Authoring Environment for Human-Robot Interaction
David Porfirio, Laura Stegner, Maya Cakmak, Allison Sauppé, Aws Albarghouthi, Bilge Mutlu
CHI 21 Human Factors in Computing Systems

Robustness to Programmable String Transformations via Augmented Abstract Training
Yuhao Zhang, Aws Albarghouthi, Loris D'Antoni
ICML 20 Machine learning / code

Generating Programmatic Referring Expressions via Program Synthesis
Jiani Huang, Calvin Smith, Osbert Bastani, Rishabh Singh, Aws Albarghouthi, Mayur Naik
ICML 20 Machine learning / code

Proving Data-Poisoning Robustness in Decision Trees
Samuel Drews, Aws Albarghouthi, Loris D'Antoni
PLDI 20 Programming Language Design and Implementation / code

Automated tuning of query degree of parallelism via machine learning
Zhiwei Fan, Rathijit Sen, Paraschos Koutris, Aws Albarghouthi
aiDM@SIGMOD 20 Artificial Intelligence Techniques for Data Management

Synthesizing Action Sequences for Modifying Model Decisions
Goutham Ramakrishnan, Yunchan Lee, Aws Albarghouthi
AAAI 20 Artificial Intelligence / code

Transforming Robot Programs Based on Social Context
David Porfirio, Allison Sauppé, Aws Albarghouthi, Bilge Mutlu
CHI 20 Human Factors in Computing Systems / code

Bodystorming Human-Robot Interactions
David Porfirio, Evan Fisher, Allison Sauppé, Aws Albarghouthi, Bilge Mutlu
UIST 19 User Interface Software and Technology / code

Synthesizing Differentially Private Programs
Calvin Smith, Aws Albarghouthi
ICFP 19 Functional Programming / code

Efficient Synthesis with Probabilistic Constraints
Aws Albarghouthi, Loris D'Antoni, Samuel Drews
CAV 19 Computer Aided Verification / code

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

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 / code

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 / code
🏆 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 / code

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 / code

Discovering Relational Specifications
Calvin Smith, Gabriel Ferns, Aws Albarghouthi
FSE 17 Foundations of Software Engineering / code
🏆 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 / code

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

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 / code

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
has since been implemented as an optimization engine in Z3

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

Current students

Samuel Drews
Zhiwei Fan
Anna Meyer
David Porfirio
Yuhao Zhang
Jinman Zhao

Former students

Calvin Smith (PhD, 20) ➞ Postdoc at UT Austin
Goutham Ramakrishnan (MSc, 20) ➞ ML Engineer at Health[at]Scale
Yun Chan Lee (MSc, 19) ➞ Software Developer at AWS

Awards

20 Facebook probability & programming research award
20 Facebook probability & programming research award
19 Facebook probability & programming research award
18 Best paper award at UIST
18 Best paper award at FAST
17 Best paper award at FSE
17 NSF CAREER award
16 Google faculty research award
13 SV-COMP 4 gold medals

Teaching

F20 CS 536: Intro to Compilers and Programming Languages
S20 CS 839: Verified Deep Learning
F19 CS 536: Intro to Compilers and Programming Languages
S19 CS 704: Principles of Programming Languages
F18 CS 536: Intro to Compilers and Programming 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

21 MAPL (publicity chair), VMCAI, IJCAI, AAAI, FAccT
20 PLDI, CAV, FoMLAS (co-chair), MAPL, ICFP (ERC), PPAI@AAAI
19 POPL, FAT* (track co-chair), CAV, VSTTE, TPDP
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

The name

My first name rhymes with house—i.e., pronounced ouse. Aws is an ancient Arabic word for wolf. The first recorded mention of Aws that I'm aware of is in a Graeco-Arabic inscription. My last name is pronounced Al·bar·goo·ti (or Bar·goo·ti). Albarghouthi is a Palestinian family from the village of Deir Ghassaneh, about 20 miles north of Jerusalem and east of Jaffa.

Misc

To my knowledge, my PhD thesis (p. 77) is the first CS thesis to cite Jay Z