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.

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.

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