Sketching robot programs on the fly

Crowdsourcing task traces for service robotics

BagFlip: A certified defense against data poisoning

AutoWS-Bench-101: Benchmarking Automated Weak Supervision with 100 Labels

Qubit mapping and routing via MaxSAT

Interval universal approximation for neural networks

Semantic robustness of models of source code

Backdoors in neural models of source code

Certifying robustness to programmable data bias in decision trees

Certified robustness to programmable transformations in LSTMs

Interaction templates: A data-driven approach for authoring robot programs

Figaro: A tabletop authoring environment for human-robot interaction

Learning differentially private mechanisms

Distribution policies for datalog

Synthesizing action sequences for modifying model decisions

Transforming robot programs based on social context

Generating programmatic referring expressions via program synthesis

Robustness to programmable string transformations via augmented abstract training

Proving data-poisoning robustness in decision trees

SIGPLAN Research Highlight / Appeared in Communications of the ACM (CACM), Feb 2023

Automated tuning of query degree of parallelism via machine learning

Synthesizing differentially private programs

Trace abstraction modulo probability

Scaling up in-memory datalog processing: Observations and techniques

Efficient synthesis with probabilistic constraints

Fairness-aware programming

Computational tools for human-robot interaction design

Bodystorming human-robot interactions

Program synthesis with equivalence reduction

Synthesizing coupling proofs of differential privacy

Protocol-aware recovery for consensus-based distributed storage

Constraint-based synthesis of coupling proofs

Protocol-aware recovery for consensus-based storage

Best paper award

Distribution policies for datalog

Fairness: A formal-methods perspective

Neural-augmented static analysis of android communication

Syntax-guided synthesis of datalog programs

Authoring and verifying human-robot interactions

Best paper award

FairSquare: Probabilistic verification of program fairness

Repairing decision-making programs under uncertainty

Constraint-based synthesis of datalog programs

Weighted model integration with orthogonal transformations

Probabilistic horn clause verification

Discovering relational specifications

Best paper award

Effectively propositional interpolants

MapReduce program synthesis

Maximal specification synthesis

Beyond storage apis: Provable semantics for storage stacks

Spatial interpolants

Symbolic optimization with SMT solvers

Beautiful interpolants

Recursive program synthesis

UFO: verification with interpolants and abstract interpretation

Winner of 4 gold medals and 1 bronze medal

Ufo: A framework for abstraction- and interpolation-based software verification

Parallelizing top-down interprocedural analyses

Craig interpretation

From under-approximations to over-approximations and back

Whale: An interpolation-based algorithm for inter-procedural verification

Abstract analysis of symbolic executions

On the use of planning technology for verification