A word is a sequence of symbols drawn from a finite set, and is often a device to represent the evolution of a (discretised) system. Words are central to both symbolic dynamics and verification. In the former discipline, words that represent the same system constitute a shift space, and are typically studied for their combinatorial structure. In verification, a quintessential objective is to certify that a system satisfies a logical specification by showing that its representative words are accepted by an automaton. In this thesis, we bridge the two perspectives through the following contributions.

1) We describe how the action of a deterministic finite transducer on an infinite word preserves the structure of the word. If the input word x has a recurrence property, then this property is preserved for the output word A(x); using the ergodic theory of shift spaces, we identify a large class of words x, including Sturmian words, such that A(x) is guaranteed to admit factor frequencies.

2) We show that we can determine whether an automaton accepts a word by reading its so-called S-adic construction. This allows us, e.g., to decide, given an automaton A, whether A accepts all Sturmian words, or all d-letter Arnoux-Rauzy words.

3) As applications, we study Monadic Second-Order (MSO) logic, and show that the MSO theory of the natural numbers remains decidable when expanded with the following sets of predicates: (i) powers of 2 and 3; (ii) powers of 2, 3, and 5, subject to Schanuel's conjecture; (iii) perfect squares and powers of 2, subject to the binary expansion of the square root of 2 being a disjunctive word.

What if we played a modified version of the Imitation Game, where instead of reading a textual conversation between a human and a machine, the evaluator instead evaluated the video (or VR) conversation between them? Enabling, and eventually winning, this game has been a north star in digital human research. While tremendous progress has occurred in modeling the physicality of digital humans, modeling the behaviour that drives our actions remains a challenging pursuit.

In this talk, I will discuss our ongoing works towards this goal. I will first introduce our works on character animation, and how we enable multiple modalities like text and audio to generate the animations. In the second half, I will introduce our works on co-speech gesture generation for virtual humans. The talk will accompany a demo of our work on real-time Embodied Character Agents.

The remarkable advances in AI have given rise to a growing interest in AI-assisted decision support in domains ranging from medicine and drug-discovery, to criminal justice and education. The ultimate goal in AI-assisted decision support is to optimally combine the complementary strengths of humans and AI models to achieve greater outcomes than either can achieve on their own, in short human-AI complementarity. Achieving this goal, however, has shown to be a major challenge as it typically requires human experts to understand when they can rely on the AI model for their decision—a highly non-trivial task. In this thesis, I show that it is possible to circumvent this challenge and achieve human-AI complementarity under an alternative design of decision support systems. The key innovation in this design lies in adaptively controlling the level of human agency by using an AI model to narrow down the decisions a human can take to a subset. I introduce algorithmic methods to construct as well as optimize these subsets to provably improve performance in decision-making tasks compared to the performance of the AI model used by the system or the human deciding on their own. To empirically evaluate these methods, I conduct two large-scale human subject studies that show that the proposed decision support system leads to human-AI complementarity in practice.

Cloud systems are composed of multiple inter-connected independent subsystems. These systems are complex in nature as they are made of heterogeneous components rife with complicated interactions, operate in dynamic conditions, and exhibit unpredictable behaviors. Developers expend significant manual effort to efficiently design, implement, optimize, operate, and improve these systems throughout the cloud system lifecycle.

This dissertation proposes Human-in-the-loop Specification-Driven Automation (HITLSDA) techniques for reducing the manual effort required by developers for carrying out tasks across the cloud lifecycle. HITLSDA techniques reduce the manual effort by the decoupling the creative component of cloud lifecycle tasks that require human insight from their corresponding mechanical component which can be automated.

We instantiate this HITLSDA approach through two systems targeting different phases of the cloud lifecycle: (i) Blueprint, a toolchain for generating and reconfigurable microservice systems that streamlines exploration of the cloud system design space; and (ii) Iridescent, a framework for online, workload-driven runtime specialization that continuously optimizes system performance by adapting code to observed execution behavior. Together, these systems demonstrate that HITLSDA provides a general and effective paradigm for reducing developer burden in cloud system design, implementation, and optimization while maintaining flexibility and performance.

Reinforcement learning (RL) has emerged as a fundamental approach to decision-making in machine learning, with applications across a wide range of real-world domains, and several practical extensions, such as multi-agent RL (MARL) and RL from human feedback (RLHF). Despite the growing successful applications of these systems, there exists an inherent threat when it comes to applying them in the real world, where ill-intentioned third parties may intervene in both their training process and deployment. This typically has catastrophic consequences, where even small and inexpensive perturbations to the environment may cause the system to substantially diverge from the desired behavior. The purpose of this thesis is to provide a thorough investigation of various adversarial attacks and robustness against such attacks to (MA)RL and (MA)RLHF systems. In particular, we study training-time and test-time attacks in MARL and propose algorithms that are shown to be provably robust against such attacks. Beyond MARL, we establish fundamental statistical results for RLHF, provide a rigorous characterization of poisoning attacks to RLHF, and develop robust extensions for MARLHF. Our work is centered around robust algorithmic approaches with provable guarantees under common assumptions.

Two-player games on finite graphs are the central algorithmic model of the reactive synthesis problem: av{automatically} constructing a controller that enforces a given temporal specification against every behavior of its environment. av{A faithful game model is, however, delicate: an overly powerful environment makes winning impossible, an overly weak one yields controllers that fail in practice.} \emph{Fairness assumptions} address this modeling challenge by concisely capturing realistic constraints on the environment, such as ``a request enabled infinitely often is granted infinitely often.'' The most general such notion, \emph{strong fairness}, is encoded by a Streett winning condition and makes game solving intractable. This thesis studies a structurally restricted, yet practically expressive subclass: \emph{strong transition fairness}, which attaches fairness to designated \emph{fair edges} of the game graph. Recent work has shown that for ùù-regular winning conditions such as B\"uchi, Rabin, and parity, strong transition fairness comes essentially \emph{for free}: fair games can be solved with the same algorithmic effort as their non-fair counterparts. This thesis investigates how far fairness stays free, and what its boundaries are. We start by saving a foundational result: the published equivalence between fairness and randomness turns out to rest on a false clause; we refute that clause and prove the surviving equivalence for all Muller objectives. The phenomenon extends further. Fairness may constrain both players at once, as environment assumption and system obligation: we introduce the first framework for such \emph{doubly-fair} games, give a determined semantics \dfsc{for all ùù -regular objectives} and\dfsc{, for parity,} a polynomial reduction to standard parity games. Beyond ùù-regular objectives, fair mean-payoff and energy games stay in the pseudo-polynomial regime, though one variant is, surprisingly, not determined; throughout, we settle the strategy complexity of both players. "Fairness for free'' ends twice. It ends at the arena. A complete classification of \emph{viability games} over valence systems, of independent interest, shows that fairness strictly shrinks what stays decidable: a game solvable in exponential time without fairness becomes undecidable with it. And it ends at the format. Fairness attached to a \emph{group} of edges makes game solving NP-hard already for reachability, and tractability is not preserved under products. We show that fairness is "for free'' not only on paper but also in practice: symbolic fixpoints, Zielonka's recursion, and progress measures all carry over to their fair counterparts with negligible overhead. The fair Zielonka solver matches its classical counterpart in experiments; the new progress measures drive the first incremental, data-driven synthesis framework for unknown stochastic systems, with speedups approaching two orders of magnitude.

Critical autonomous systems, such as robots operating amongst humans or a rover navigating on a remote planet, must continuously react to environments they do not control while provably satisfying their specifications. Designing a correct controller for such machines manually is impossible as a human cannot foresee every environmental possibility. Reactive synthesis provides an alternative approach of automatically building correct-by-construction controllers from formal specifications. Although this is a well-studied field, it almost entirely focuses on finding a single controller that satisfies the specification. The real world, however, is transient, and a single controller is rarely sufficient in practical applications. When an action proposed by the controller becomes unavailable (e.g., due to a component failure), the system immediately stalls, forcing an expensive re-synthesis.

This thesis addresses this problem by introducing a concise data-structure, called the strategy template, which represents infinitely many controllers. Strategy templates localize a given specification by local guidelines for a controller to choose the next action. In the first part of the thesis, we define the notion of strategy templates for major classes of specifications and models of interaction of the system and the environment. We then provide algorithms for computing the templates, and prove soundness (i.e., a controller following the template satisfies the specification) and completeness (i.e., if there is a controller that satisfies the specification, we compute a strategy template). We show that the strategy templates enable us to compose various specification online, and make controllers more robust to changes in the environment at runtime. In the second part, we utilize the resulting permissiveness (i.e., capturing infinitely many controllers) of the templates to shield learned policies which usually lack formal guarantees of correctness. The templates allow us to monitor and nudge the policies to ensure that they satisfy liveness (i.e., some progress is made), which until now had eluded the shielding literature. Furthermore, we implement all the algorithms proposed and show that they outperform the state-of-the-art in terms of composibility, robustness and scalability.

Block-based visual programming initiatives such as Hour of Code by code.org and Intro to Programming with Karel by CodeHS.com, have transformed introductory computer science education by making programming more accessible to K-8 learners. Despite their accessibility, students often struggle with multi-step reasoning and conceptual abstraction when solving open-ended tasks. Quizzes (such as fill-in-the-gap exercises, and multiple-choice conceptual questions based on code debugging and task design) offer interactive practice and targeted feedback that can promote active learning and scaffold novice programmers. However, manually designing such quizzes is time-consuming and difficult to scale. This thesis tackles these challenges by developing automated synthesis techniques for programming tasks and quizzes, and evaluates their pedagogical utility.

The first part of the thesis introduces algorithmic methods for synthesizing programming tasks and quizzes in block-based environments. Specifically, we develop methods for the following : (i) synthesizing conceptually similar and yet visually dissimilar write-code tasks; and (ii) synthesizing adaptive multiple-choice programming quizzes that address student-specific misconceptions; Each method leverages symbolic execution, sketch-based code mutation, and search-guided generation to ensure pedagogical utility, relevance, and technical correctness. Empirical evaluations conducted through controlled user studies demonstrate the efficacy of these approaches, showing that they not only support novice learners effectively but also outperform existing methods, including next-step code edit based feedback methods.

The second part of the thesis empirically evaluates the pedagogical utility of programming quizzes in these environments via user studies and classroom deployments with K-8 learners. Specifically, we examine: (i) the design, validation, and classification of quiz types using cognitive frameworks such as Bloom's Revised Taxonomy; (ii) the impact of embedding quizzes within programming curricula on post-learning outcomes; and (iii) the effectiveness of quiz-based feedback scaffolds with different quiz-types. Our findings show that quizzes designed using metacognitive strategies and adapted to learners’ attempts significantly enhance engagement and task performance. Moreover, we observe that richer and more diverse quiz types—when integrated into the curriculum—lead to improved post-learning outcomes, while simpler, less cognitively demanding quizzes may hinder post-learning performance.

Overall, this thesis contributes novel synthesis methods for programming quizzes and empirical evidence of their effectiveness in elementary-level programming education. These findings provide a foundation for scalable and adaptive support in elementary computing curricula.

A mix network (mixnet) is a routing network that conceals communication patterns by shuffling, or mixing, the routes of concurrently transmitted messages, thereby providing anonymity for senders, receivers, and sender-receiver pairs. Notable examples of deployed mixnets are Tor and Nym. Given the potential use of mixnets in high-stakes applications, such as protecting whistleblowers, it is essential to establish formal guarantees of sender anonymity, even against powerful adversaries that have a full view of the network and are capable of compromising subsets of mix servers. However, existing analyses of mixnets anonymity typically rely on additional mechanisms, such as noise or chaff messages, or are based on empirical metrics such as entropy, which cannot provide strong guarantees in the presence of adversaries with auxiliary information. My thesis consists of two complementary parts: (1) a first part on parallel mixnets, in which mix nodes operate in loosely synchronized rounds, and (2) a second part on continuous-time mixnets, in which mix nodes operate independently and forward messages after user-specified random delays. First, I present a new analysis of horizontally scalable parallel mixnets, showing that they can achieve strong indistinguishability guarantees for messages without requiring additional noise messages or extensive cryptographic techniques. Second, I develop a theoretical framework for continuous-time mixing by identifying two interacting stochastic processes that govern mixnets' operation: a local shuffling process at each mix node, driven by message delays and their sampling, and a global shuffling process that determines how messages (or batches) propagate between mixing layers. Building on this perspective, I derive a new tractable analytical model that captures mixing at both the local (per-node) and global (system-wide) levels. Finally, I use this model to establish provable anonymity guarantees for asynchronous mixnets.

AI-driven systems increasingly shape consequential decisions in domains such as lending, university admissions, and content moderation. Yet making these systems trustworthy in practice requires more than principled algorithms: it requires methods that scale, account for bias throughout the decision-making process, and can be evaluated against deployed real-world systems. This thesis addresses these challenges through three lines of work: scalable causal algorithmic recourse, fairness across the decision-making pipeline, and content policy enforcement on digital platforms.

First, it introduces CARMA, a neural-network-based approach that amortizes causal recourse generation, producing near-real-time recommendations while preserving causal validity and effort optimality. Second, it addresses fairness across the decision-making pipeline by developing a causal framework for measuring and mitigating bias in post-selection treatment decisions, alongside an online learning framework, FairAll, that learns fair and temporally consistent selection policies without sacrificing utility. Third, it studies instruction-driven moderation with foundation models and introduces ModerationBench, a benchmark of multimodal, in-the-wild social media content grounded in Bluesky’s deployed moderation guidelines.

Together, these contributions push Responsible AI beyond idealized settings and toward practical deployment. They provide scalable mechanisms for recourse, broader tools for fairness across the full decision-making pipeline, and grounded methods for evaluating adaptable content-safety enforcement in real-world digital platforms.

Multi-pushdown automata (MPDA) are a classic computational model that can be used to capture the behavior of multithreaded recursive programs. Here, each parallel thread is simply modeled by a single stack, and there is a fixed number of them. Due to the well known fact that most verification problems are undecidable for MPDA, even with just two stacks, the literature contains many different ways to restrict the runs of this model, in such a manner as to recover decidability. A popular restriction of this kind is known as bounded context-switching: For a fixed bound k, every parallel thread (or stack) may only be interrupted by another thread up to k times.

We consider an extended setting, where the number of parallel threads is not fixed, and more of them can be spawned dynamically during execution. This gives rise to the model of dynamic networks of concurrent pushdown systems (DCPS), which we still restrict with bounded context-switching. In this setting, we consider various verification questions, that have been asked for similar models in the past. These include state reachability, non-termination (with and without assumptions on fairness), and boundedness of the thread buffer. Moreover we consider the novel verification problem of Dyck inclusion: Given a model with action sequences over some alphabet of bracket pairs, are all its executions well-bracketed? Our results close a preexisting complexity gap for state reachability, and settle the complexity of several other verification problems, where in many cases even decidability was unknown before

Software is what turns quantum hardware into technology everyone can use. In this talk we focus on the quantum communication networks, with the first metropolitan scale quantum networks being built and the technologies to connect them over long distances advancing. We begin with the first operating system for quantum networks (QNodeOS), allowing applications to be programmed and executed on arbitrary quantum processors connected to a quantum network. Demonstrated on two different types of quantum hardware, QNodeOS now provides a framework for experimenting with software systems for quantum networks. We then turn to a specific kind of quantum network application, in which entanglement is harnessed for coordination between distant parties. We explore this through a recent example in radio spectrum allocation, opening the door to a new domain of quantum network applications.

Put yourself in the shoes of an algorithm designer working on some computational problem. You have found an algorithm running in time O(n^2), say, but after months of effort no faster algorithm is in sight. Perhaps your algorithm is already optimal – but how could you show this? This is the central challenge of fine-grained complexity theory. In the spirit of classical NP-hardness, this theory starts from the assumption that certain canonical problems are hard, and then uses so-called fine-grained reductions to show that many other problems are conditionally hard as well.

In this talk, I will first describe the basic concepts of fine-grained complexity along with some illustrative examples, before turning to more recent developments, including some of my own work. I will discuss some questions that resisted the basic theory for a long time, and how progress on them has required a more sophisticated method – the celebrated structure-versus-randomness paradigm.