Aws Albarghouthi
Associate Professor
Computer Sciences
UW–Madison
I study the art and science of program synthesis and verification.
My group is currently focused on two problems:
a) automatically synthesizing compilers for quantum computers
and b) certifying robustness and fairness of machine learning.
I'm always looking for ambitious students.
I'm currently on leave at
AWS (I know, hilarious).
cv ·
blog ·
aws@cs.wisc.edu
🔥 News
07.24
Gave a
talk at PLMW in Copenhagen on my scientific journey
04.23
Lauren has two papers at PLDI 🤩!
04.23
Anna's paper on data bias will appear at FAccT!
04.23
Amanda's paper on quantum optimization will appear at PLDI!
📚 Books
Introduction to neural network verification
Aws Albarghouthi
📝 Papers
see all papers · preprints on arxiv
Optimizing quantum circuits, fast and slow
ASPLOS 25 · Xu, Molavi, Tannu, Albarghouthi
The dataset multiplicity problem: How unreliable data impacts predictions
FACCT 23 · Meyer, Albarghouthi, D’Antoni
Synthesizing quantum-circuit optimizers
PLDI 23 · Xu, Molavi, Pick, Tannu, Albarghouthi
Proving data-poisoning robustness in decision trees
CACM 23 · Drews, Albarghouthi, D’Antoni
🏆 Research highlight
Sketching robot programs on the fly
HRI 23 · Porfirio, Stegner, Cakmak, Sauppé, Albarghouthi, Mutlu
Crowdsourcing task traces for service robotics
HRI 23 · Porfirio, Sauppé, Cakmak, Albarghouthi, Mutlu
BagFlip: A certified defense against data poisoning
NeurIPS 22 · Zhang, Albarghouthi, D’Antoni
AutoWS-Bench-101: Benchmarking Automated Weak Supervision with 100 Labels
NeurIPS 22 · Roberts, Li, Huang, Adila, Schoenberg, Liu, Pick, Ma, Albarghouthi, Sala
Qubit mapping and routing via MaxSAT
MICRO 22 · Molavi, Xu, Diges, Pick, Tannu, Albarghouthi · code
Interval universal approximation for neural networks
POPL 22 · Wang, Albarghouthi, Prakriya, Jha
Semantic robustness of models of source code
SANER 22 · Henkel, Ramakrishnan, Wang, Albarghouthi, Jha, Reps · code
Backdoors in neural models of source code
ICPR 22 · Ramakrishnan, Albarghouthi · code
Certifying robustness to programmable data bias in decision trees
NeurIPS 21 · Meyer, Albarghouthi, D’Antoni · code
Certified robustness to programmable transformations in LSTMs
EMNLP 21 · Zhang, Albarghouthi, D’Antoni · code
Interaction templates: A data-driven approach for authoring robot programs
PLATEAU 21 · Porfirio, Cakmak, Sauppé, Albarghouthi, Mutlu
Figaro: A tabletop authoring environment for human-robot interaction
CHI 21 · Porfirio, Stegner, Cakmak, Sauppé, Albarghouthi, Mutlu · code
Learning differentially private mechanisms
SP 21 · Roy, Hsu, Albarghouthi
Distribution policies for datalog
TOCS 20 · Ketsman, Albarghouthi, Koutris
Synthesizing action sequences for modifying model decisions
AAAI 20 · Ramakrishnan, Lee, Albarghouthi · code
Transforming robot programs based on social context
CHI 20 · Porfirio, Sauppé, Albarghouthi, Mutlu · code
Generating programmatic referring expressions via program synthesis
ICML 20 · Huang, Smith, Bastani, Singh, Albarghouthi, Naik · code
Robustness to programmable string transformations via augmented abstract training
ICML 20 · Zhang, Albarghouthi, D’Antoni · code
Proving data-poisoning robustness in decision trees
PLDI 20 · Drews, Albarghouthi, D’Antoni · code
🏆 SIGPLAN Research Highlight / Appeared in Communications of the ACM (CACM), Feb 2023
Automated tuning of query degree of parallelism via machine learning
AIDM 20 · Fan, Sen, Koutris, Albarghouthi
Synthesizing differentially private programs
ICFP 19 · Smith, Albarghouthi · code
Trace abstraction modulo probability
POPL 19 · Smith, Hsu, Albarghouthi
Scaling up in-memory datalog processing: Observations and techniques
VLDB 19 · Fan, Zhu, Zhang, Albarghouthi, Koutris, Patel · code
Efficient synthesis with probabilistic constraints
CAV 19 · Drews, Albarghouthi, D’Antoni · code
Fairness-aware programming
FAT* 19 · Albarghouthi, Vinitsky
Computational tools for human-robot interaction design
HRI 19 · Porfirio, Sauppé, Albarghouthi, Mutlu
Bodystorming human-robot interactions
UIST 19 · Porfirio, Fisher, Sauppé, Albarghouthi, Mutlu · code
Program synthesis with equivalence reduction
VMCAI 19 · Smith, Albarghouthi · code
Synthesizing coupling proofs of differential privacy
POPL 18 · Albarghouthi, Hsu
Protocol-aware recovery for consensus-based distributed storage
TOS 18 · Alagappan, Ganesan, Lee, Albarghouthi, Chidambaram, Arpaci-Dusseau, Arpaci-Dusseau
Constraint-based synthesis of coupling proofs
CAV 18 · Albarghouthi, Hsu
Protocol-aware recovery for consensus-based storage
FAST 18 · Alagappan, Ganesan, Lee, Albarghouthi, Chidambaram, Arpaci-Dusseau, Arpaci-Dusseau
🏆 Best paper award
Distribution policies for datalog
ICDT 18 · Ketsman, Albarghouthi, Koutris
Fairness: A formal-methods perspective
SAS 18 · Albarghouthi
Neural-augmented static analysis of android communication
FSE 18 · Zhao, Albarghouthi, Rastogi, Jha, Octeau
Syntax-guided synthesis of datalog programs
FSE 18 · Si, Lee, Zhang, Albarghouthi, Koutris, Naik · code
Authoring and verifying human-robot interactions
UIST 18 · Porfirio, Sauppé, Albarghouthi, Mutlu · code
🏆 Best paper award
FairSquare: Probabilistic verification of program fairness
OOPSLA 17 · Albarghouthi, D’Antoni, Drews, Nori · code
Repairing decision-making programs under uncertainty
CAV 17 · Albarghouthi, D’Antoni, Drews · code
Constraint-based synthesis of datalog programs
CP 17 · Albarghouthi, Koutris, Naik, Smith · code
Weighted model integration with orthogonal transformations
IJCAI 17 · Merrell, Albarghouthi, D’Antoni
Probabilistic horn clause verification
SAS 17 · Albarghouthi
Discovering relational specifications
FSE 17 · Smith, Ferns, Albarghouthi · code
🏆 Best paper award
Effectively propositional interpolants
CAV 16 · Drews, Albarghouthi
MapReduce program synthesis
PLDI 16 · Smith, Albarghouthi · code
Maximal specification synthesis
POPL 16 · Albarghouthi, Dillig, Gurfinkel
Beyond storage apis: Provable semantics for storage stacks
HotOS 15 · Alagappan, Chidambaram, Pillai, Albarghouthi, Arpaci-Dusseau, Arpaci-Dusseau
Spatial interpolants
ESOP 15 · Albarghouthi, Berdine, Cook, Kincaid
Symbolic optimization with SMT solvers
POPL 14 · Li, Albarghouthi, Kincaid, Gurfinkel, Chechik
Beautiful interpolants
CAV 13 · Albarghouthi, McMillan
Recursive program synthesis
CAV 13 · Albarghouthi, Gulwani, Kincaid
UFO: verification with interpolants and abstract interpretation
TACAS 13 · Albarghouthi, Gurfinkel, Li, Chaki, Chechik
🏆 Winner of 4 gold medals and 1 bronze medal
Ufo: A framework for abstraction- and interpolation-based software verification
CAV 12 · Albarghouthi, Li, Gurfinkel, Chechik
Parallelizing top-down interprocedural analyses
PLDI 12 · Albarghouthi, Kumar, Nori, Rajamani
Craig interpretation
SAS 12 · Albarghouthi, Gurfinkel, Chechik
From under-approximations to over-approximations and back
TACAS 12 · Albarghouthi, Gurfinkel, Chechik
Whale: An interpolation-based algorithm for inter-procedural verification
VMCAI 12 · Albarghouthi, Gurfinkel, Chechik
Abstract analysis of symbolic executions
CAV 10 · Albarghouthi, Gurfinkel, Wei, Chechik
On the use of planning technology for verification
VVPS 09 · Albarghouthi, Baier, Mcilraith
🎓 Research group
Abtin Molavi
Amanda Xu
Anna P. Meyer
Yuhao Zhang · PhD 24 ➞ Scientist at AWS
Lauren Pick · Postdoc 24 ➞ Assistant Professor at CUHK
David Porfirio · PhD 22 ➞ Researcher at The Naval Research Lab
Samuel Drews · PhD 21 ➞ Software Engineer at Facebook
Jinman Zhao · PhD 21 ➞ Scientist at AWS
Calvin Smith · PhD 20 ➞ Postdoc at University of Texas, Austin
Goutham Ramakrishnan · MSc 20 ➞ ML Engineer at Health at Scale
Yun Chan Lee · MSc 19 ➞ Software Engineer at AWS
🏆 Awards
22
Amazon Research Award
22
Class of 1955 Teaching Excellence Award
21
SIGPLAN research highlight for PLDI 20 paper
20
Facebook programming languages and probability award
20
Facebook programming languages and probability award
19
Facebook programming languages and probability award
18
UIST Best paper award
18
FAST Best paper award
17
FSE Best paper award
17
NSF CAREER award
16
Google faculty research award
13
SV-COMP Winner of 4 gold medals and 1 bronze medal
10
Alexander Graham Bell Canada graduate scholarship
✏️ Teaching
S22
CS 704: Principles of programming languages
🍉 The name ·
أوس البرغوثي
My first name rhymes with house—i.e., pronounced ouse.
Aws is an ancient Arabic word for wolf.
See, for example, this Graeco-Arabic inscription.
My last name is pronounced Al·bər·go͞o·tē (or Bər·go͞o·tē).
Albarghouthi is a Palestinian family from the village of Deir Ghassaneh, about 20 miles north of Jerusalem and east of Jaffa.
♾️
To my knowledge, my
PhD thesis (p. 77) is the first CS
thesis to cite Jay Z
Page layout is a fork of
minimal (
CC BY-SA 3.0)