I work at the intersection of programming languages, compilers, and software engineering. I am pursuing an ambitious research agenda that rethinks programming systems for modern applications in which noisy data, unreliable communication, approximate computation, and uncertain decisions are fundamental traits. Such applications are pervasive in many fields, including machine learning, data analytics, multimedia processing, and robotics. My research aims to attack three “grand challenges” for future programming systems – including languages, compilers, runtime systems, developer-productivity tools, and software-hardware interfaces:

How can the next-generation programming systems and hardware interoperate to give acceptably accurate results with maximum performance and energy savings?

How can these systems rigorously quantify the inaccuracy and noise from the inputs and computation?

How to apply these principles to improve the reliability of software operating in uncertain environments?

My research seeks to answer these questions by combining empirical techniques from programming languages and computer systems with solid mathematical foundations provided by probability theory, mathematical optimization, logic, and statistics. At Illinois, my work redesigns the entire computing stack, from applications to hardware, with the abstractions for approximation and uncertainty as central tenets.

I have published my research broadly, in top conferences in programming languages (PLDI, POPL, OOPSLA, ASPLOS, PPoPP, ESOP, ECOOP, CGO, SAS) and software engineering (FSE, ICSE, ISSTA, ICST), but also in formal methods (CAV, ATVA, RV), computer architecture (HPCA), high-performance computing (ICS), computer systems (USENIX ATC), and embedded systems (DAC). As of December 2021, my papers have accumulated over 3500 citations according to Google Scholar (eleven papers have over 100 citations each) and my h-index is 25. Three papers won Distinguished paper awards [OOPSLA’13, OOPSLA’14, ICSE-NIER’20] and one was recognized with the Test-of Time honorable mention [FSE’11]. My group's research has been funded by NSF, DARPA, USDA, and industry gifts. My tools, which are publicly available, have helped identify significant performance improvement opportunities and exposed numerous accuracy-related errors in existing software. My work at the University of Illinois has explored three main directions:

Programming systems for principled computing with approximations;

Programming systems for reliable and efficient probabilistic software;

Programming systems for improving software reliability, including support for autonomous distributed systems.

Approximate computing explores various system-level techniques for reducing the time and energy of the computation by trading off a small level of accuracy. My Ph.D. work pioneered accuracy-aware compiler transformations and probabilistic accuracy analyses [MITTR'09, ICSE’10, ASPLOS’11, FSE’11, SAS’11, POPL’12, PLDI’12, RACES’12, TECS’13, OOPSLA’13, OOPSLA’14, MITPHD'15, CACM’16]. An interested reader may find the brief summary of these contributions here. While the community developed many promising early results at individual levels of the computing stack, it remained an open question how to safely apply and systematically compose different approximations, especially for parallel and heterogeneous systems (most previous analyses focused on sequential programs). At Illinois, I have been working on building a practical ecosystem of techniques for principled program approximation. My goal is to simplify the development of approximate programs by helping programmers ensure safety and quantitative reliability as well as manage accuracy-performance tradeoffs on parallel and heterogeneous hardware. To accomplish this goal, my research extends across the full computing stack.

We designed the first *language/verification*** system**
for reasoning about approximate asynchronous message-passing programs [OOPSLA’19a].
We show that a handful of language constructs (typed channels, conditional
send/receive primitives, and random choice) are general enough to express most
communication-oriented approximations proposed in the literature. We designed a
novel automated sequentialization approach that enables lifting an arbitrary
sequential approximation analysis to reason about message-passing programs that
satisfy the symmetric nondeterminism property. It also ensures that the
approximations do not cause deadlocks. We demonstrated the effectiveness and
generality of our approach by representing and proving the correctness of four
analyses in our system – approximation types, relative safety, reliability, and
accuracy – and using them jointly to automatically verify eight approximate
programs and eight common parallel kernels for various communication-oriented
approximations. We also extended the language with recovery blocks and a
precise quantitative reliability analysis [CGO’20], and incorporated
low-overhead runtime accuracy monitoring [RV’21].

We developed a novel ** compiler **for
heterogeneous systems with approximate hardware (e.g., custom accelerators) and
software components (e.g., algorithmic approximation). They tackle the
challenges of navigating large tradeoff spaces induced by approximations and
maintaining accuracy/performance portability across different hardware
platforms. We designed a set of LLVM IR extensions for tensor-based programs
augmented with accuracy specifications, and developed a three-level predictive
auto-tuning approach for the combination of hardware-agnostic (that may be
known ahead of time,

We built adaptive ** runtime systems** for input-aware and
phase-aware approximation that leverage the dynamic changes of accuracy at
run-time and thus provide finer-grained control of the result accuracy. For
video processing pipelines, we expose input-awareness via error calibration
(inspired by ’canary inputs’) on adaptively sampled frames [ATC’18].
For graph analytics programs, our input-aware algorithm systematically reduces
a graph during pre-processing, and uses an adaptive post-processing scheme to
improve the final result [ICS’20]. For
iterative numerical programs, our runtime system adapts approximation level in
each identified execution phase (e.g., beginning, middle, or end) [CGO’17].

We co-designed a new ** shared-memory multiprocessor**
with a wireless network-on-chip, and developed a programming model and runtime
system that leverage approximate communication [ASPLOS’19a,
HPCA’21].
Each CPU core is equipped with a wireless antenna that broadcasts select data
to the other cores and can selectively drop messages to reduce contention on
the wireless channel. Our programming system automatically identifies data in
shared-memory programs that can benefit from wireless communication and/or
tolerate dropped messages. For a set of graph and scientific benchmarks, it
achieved ~1.9x speedup (with high accuracy) over the conventional architecture
with wired network-on-chip.

Probabilistic algorithms emerged in various areas of computer science. Notably, probabilistic programming (PP) aims to democratize Bayesian inference by representing complex models as simple high-level programs, while the underlying PP systems hide the intricate details of inference. PP has recently shown exciting potential and gained significant interest from industry (e.g., Facebook, Google, Microsoft, Uber) and the scientific community (e.g., epidemic modeling and single-cell genomics). However, this area is still in its infancy and needs an ecosystem of tools for improving the reliability and accuracy of PP systems. My work identified that many errors that occur in probabilistic computations and underlying systems are caused by randomness and/or handling of probability distributions and are hard to identify using conventional testing and analysis approaches. My research presents novel techniques for testing probabilistic algorithms and systems [FSE’18, ICSE’19, FSE’19, ISSTA’20, ISSTA’21, FSE’21] and novel analyses for reasoning about the accuracy of probabilistic programs [ATVA’18, PLDI’18, ESOP’20, ATVA’21, DAC’21].

We developed the ** foundation for testing PP systems** [FSE’18].
Our fuzzing-based framework has several analogies with compiler fuzz-testing.
However, to make fuzzing effective for PP systems, we show the necessity to
incorporate domain-specific information about probability distributions,
dependence analysis, and accuracy tests to guide the search for errors. It
helped us discover and fix over 50 new bugs in three popular PP systems (Stan,
Pyro, Edward) and two underlying libraries (PyTorch and TensorFlow). We also
made a taxonomy of all errors previously reported in these systems that can
help researches in the future. To help debug PP systems, we extended our system
with an analysis-driven algorithm for reducing error-revealing probabilistic
programs [FSE’19].

We developed new programming systems that *make*** testing
of probabilistic software more effective and easier to understand**.
While many probabilistic algorithms come with nice theoretical guarantees
(e.g., Bloom filters, locality sensitive hashing), these specifications are
rarely used to check the algorithm implementations. We thus developed a
specification language for probabilistic accuracy predicates and a framework
that checks if the specification is correct using statistical hypothesis
testing [ICSE’19].
It helped us find and fix five previously unknown bugs in popular
implementations of probabilistic algorithms. However, even if a randomized program
is correct, its tests may occasionally fail (i.e., be flaky). We developed an
approach that uses statistical convergence testing to identify flaky tests in
PP and machine learning (ML) systems [ISSTA’20],
which detected 11 new flaky tests. We extended this approach to optimize test
run time [ISSTA’21],
resulting in 2.2x speedup on 160 tests. Inspired by these works, we recently
developed the first approach for fixing assertion bounds in PP and ML systems
based on Extreme value theory from statistics, which proposed fixes to 28 tests [FSE’21].

We leveraged static analysis to ** improve the accuracy and
performance of probabilistic programs**. Building on our symbolic solver
for probabilistic programs [CAV’16], we
developed analyses for symbolic inference with accuracy guarantees [ATVA’21], symbolic sensitivity
analysis of PP’s result to noise in the inputs or prior distributions [ATVA’18] and
a domain-specific language for reasoning about congestion and reliability in
software-defined networks [PLDI’18].
We further identified accuracy issues when naively converting mixed
discrete/continuous programs to continuous (for which inference is faster). Our
approach poses PP continualization as a program synthesis problem, which
combines program analysis and numerical optimization with the aim to minimize the
accuracy loss of continualized programs [ESOP’20].
Recently, we developed an optimizing PP compiler for embedded systems that
tunes inference code to optimally use fixed-point arithmetic [DAC’21].
It achieved speedups over floating-point code of ~11x on Arduino, ~4x on PocketBeagle,
and ~2x on Raspberry Pi systems.

My research also investigated techniques for *coping
with uncertainty from the environment*** that can impact computation and
its accuracy**. Distributed robotic applications are a prominent example
with noisy sensors, ad-hoc interfaces to hardware, and potentially unreliable
communication to other robots. We developed a novel language and verification
system [OOPSLA’20]
with abstractions to make the control and coordination code portable and
modularly verifiable. Our abstractions for platform-independent code include
port interfaces for sensing and control and distributed shared memory for
coordination. We defined an executable formal semantics in the K framework. Our
formalization enables the developer to explicitly identify the assumptions
about the environment needed to prove important safety properties using
off-the-shelf solvers (e.g., for reachability) in distributed delivery and mapping
applications.

The ability of programs to
produce multiple acceptable results opens new opportunities to ** redefine
the goals of program testing and synthesis through the lens of uncertainty**.
Resiliency analysis (which studies the impact of non-deterministic soft errors
on program reliability) and approximate program analysis are similar in that
both have the notion of acceptable errors, while the inaccuracy sources are
different (bit flips vs. intentional approximations). We showed how to adapt
several foundational techniques from software testing to speed up error
injection campaigns for resiliency analysis [ASPLOS’19b, DSN’19].
We refined example-based synthesis by identifying perturbation properties that
relate changes in program outputs to those in program inputs and automatically
generating new input-output examples to reduce ambiguity [POPL’20].

The growing complexity of software and diversity of hardware platforms will continue to make uncertainty and approximation central concerns in computer systems. Many emerging applications will be distributed, adaptive, and autonomous, where each component (e.g., for perception, control, and decision-making) will require different mathematical and empirical tools that need to be combined for the end-to-end analysis and optimization in the face of uncertainty. The long-term goal of my research is to redefine programming systems to support such complex applications while being able to ensure safety and at the same time discover profitable tradeoffs between important quantitative properties – accuracy, robustness, security, privacy, and others. To support this goal, in the near future, my research will explore the three lines of work that I describe next.

The first line of work will ** build robust programming systems
to sustain the democratization of programming with probabilities**,
developed on solid theoretical foundations. The shift of computing toward AI
and machine learning is opening the need for probabilistic and statistical
reasoning. Many seasoned and novice programmers alike have little experience
with this kind of reasoning and will significantly benefit from automated
programming systems. I plan to develop approaches for systematic analysis,
testing, debugging, and repair of probabilistic software by combining both
data-driven and static analysis to obtain acceptable accuracy and scalability (e.g., by continuing from FSE’18, FSE’19, ICSE’19, ISSTA’20, ATVA’21, ISSTA’21, and FSE’21).

The second line of work will ** expand the reach of automated
probabilistic reasoning to improve reliability and performance of distributed
autonomous applications**. Autonomous robotics applications have multiple complex components and
reasoning about their fault tolerance poses new challenges. I plan to build on OOPSLA’20
work to define new domain-specific languages (e.g., for precision agriculture
and drone operation) and extend the languages and verification with
probabilistic abstractions for distributed computations (inspired by PLDI’18 and
OOPSLA’19a).
I also plan to efficiently compile high-level languages (based on OOPSLA’19b,
PPoPP’21, and
DAC’21),
while enabling low-overhead accuracy monitoring and energy-efficient inference.

The third line of work will ** invent new foundational techniques for
analyzing and optimizing quantitative tradeoffs spanning parallel/distributed
programs and hardware on which they run**. I will explore the
abstractions and interfaces between the layers of the computing stack, as well
as mathematical optimization approaches for multi-objective program tuning. I
will establish a stronger connection between quantitative program properties
and costs of computation and communication. Combining (soft) probabilistic and
(hard) logic constraints with a combination of empirical or surrogate
accuracy/performance/robustness models (e.g., by extending the approach from PPoPP’21) opens
an interesting venue for work on future adaptive analysis/optimization algorithms
that can further incorporate user feedback (e.g., as in POPL’20)
to improve their precision.