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.

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.

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.