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.

Generative AI holds great promise in enhancing programming education by automatically generating personalized feedback for students. However, ensuring that this feedback is both technically accurate and pedagogically effective remains a critical challenge before these systems can be safely deployed in real-world classrooms. This thesis investigates the end-to-end integration of generative AI in programming education, divided into two main parts.

The first part focuses on the optimization of AI-generated feedback quality. We introduce novel techniques that not only enhance the generated feedback but also perform automatic validation of the feedback before returning it. Specifically, to improve feedback quality, our techniques contextualize the prompt with similar examples from the database and uses symbolic information of failing test cases and fixes. Next, to validate the quality of AI-generated feedback, they leverage another AI agent as simulated students in a run-time validation mechanism. These techniques achieve high-precision, human tutor-style feedback.

The second part transitions to the deployment of the feedback systems in real-world classroom settings, focusing on student-instructor-AI interaction. Specifically, to ensure feedback meets both expert educators' and students' quality standards, we investigate the discrepancies between expert-created rubrics and student perceptions of hint helpfulness. To understand how to position AI-generated hints with traditional pedagogical practices, we examine the interplay between AI-generated hints and student reflection. To address the problem of students being over-reliant on AI support, we base our design on metacognitive theory to introduce different hint types with quotas to require students' critical engagement during interaction with the system. Finally, to ensure students receive relevant support in difficult cases when AI is insufficient, we propose a hybrid instructor-in-the-loop escalation mechanism, allowing instructors to efficiently involve and support students when most needed.

Ultimately, this thesis provides a foundational framework for deploying LLMs that balance automated efficiency with established pedagogical standards and human oversight.

Floating-point numbers often represent real numbers in computer systems. They are applicable in many domains, including embedded systems, machine learning, and scientific computing. Despite their widespread use, they pose some difficulties. Floating-point numbers and operations typically suffer from roundoff errors, making computations over floating-points inaccurate with respect to a real-valued specification. Moreover, the IEEE 754 floating-point standard, a fundamental element in formalizing floating-point arithmetic for today’s computers, presents additional challenges due to special values and resulting unintuitive behaviors. This thesis has three main contributions that address existing gaps in automated reasoning about floating-point arithmetic, making it easier for developers and researchers to understand, verify, and trust the floating-point computations in their programs. First, we introduce the first floating-point support in a deductive verifier for the Java programming language. Our support in the KeY verifier automatically handles floating-point arithmetic and transcendental functions. We achieve this with a combination of delegation to external SMT solvers on one hand, and rule-based reasoning within KeY on the other, exploiting the complementary strengths of both approaches. As a result, this approach can prove functional floating-point properties for realistic programs. Second, inspired by KeY’s treatment of method calls and the need for a scalable roundoff error analysis, we present the first modular optimization-based roundoff error analysis for non-recursive procedural floating-point programs. Our key idea is to achieve modularity while maintaining reasonable accuracy by automatically computing procedure summaries that are a function of the input parameters. Technically, we extend an existing optimization-based roundoff error analysis and show how to effectively use first-order Taylor approximations to compute precise procedure summaries, and how to integrate those to obtain end-to-end roundoff error bounds. Third, our experience using SMT solvers to discharge KeY’s floating-point verification conditions revealed unexpected performance behavior, motivating a systematic study of floating-point reasoning in SMT solvers. We propose a metamorphic testing approach that uses semantics-preserving rewrite rules, focusing on floating-point special values, to uncover unexpected performance behavior in SMT solvers’ handling of floating-point formulas, such as an increase in solving time when the SMT queries are simplified. Using real-world test inputs, our approach can identify such performance bugs for every SMT solver tested.

The synthesis of logical controllers that guarantee desired specifications is a central problem in the design of cyber-physical systems (CPS). In practice, such guarantees rely on assumptions about how the controller interacts with its environment. These assumptions restrict environment behavior to make synthesis feasible, but in existing approaches they are often overly restrictive, leading to conservative designs and limiting the range of behaviors that systems can safely accommodate.

This thesis rethinks the role of assumptions in logical controller synthesis by emphasizing their \emph{permissiveness}---the ability to capture a wide range of admissible environment behaviors. We study permissive assumptions in two key settings: (a) interactions among multiple discrete components in distributed systems, and (b) interactions between high-level logical controllers and low-level physical dynamics in hybrid systems. In both settings, we develop theoretical and algorithmic foundations for computing and exploiting permissive assumptions to enable new design paradigms for logical controller synthesis.

For distributed systems, we define permissiveness as capturing all cooperative behaviors of other components that enable a controller to satisfy its specification. We present an algorithm for computing such assumptions in monolithic systems and extend it to distributed systems via a negotiation-based framework that iteratively constructs permissive assume-guarantee contracts for each component. These contracts enable decentralized synthesis and are applied to human-robot interaction, allowing robots to cooperate with humans whenever possible and request cooperation only when necessary.

For hybrid systems, we utilize permissive assumptions on the plant model---the abstract representation of physical dynamics---to address three key challenges. To enable seamless adaptation of controllers to changing logical contexts, i.e., changes in high-level goals or tasks, we introduce a novel synthesis framework that utilizes \emph{persistent live groups}, a class of assumptions capturing liveness properties of continuous dynamics. To improve scalability to large or uncertain plant models, we develop \emph{universal controllers} where decisions are conditioned on branching-time assumptions called \emph{prophecies}, which are learned from representative models and efficiently verified at runtime on unseen plant models. Finally, to enhance robustness under uncertainty or partial violations of assumptions on the plant model, we introduce a robust semantics for branching-time temporal logics, enabling formal reasoning about controller behavior under such violations.

Overall, this work enables correctness-by-construction synthesis while avoiding unnecessary conservatism, resulting in CPS that are more robust, scalable, and responsive.

Computers have become ubiquitous in everyday life and so have bugs in programs running on those computers. Research in the field of programming languages and verification has produced countless ways to attack the problem of software defects. This thesis concerns itself with two established techniques being applied to an unconventional setting.

Firstly, in the category of extending the applicability of program verification to more realistic settings, we demonstrate how to verify high-performance algorithms and data structures making use of highly efficient memory access patterns that are not automatically synchronized with main memory or other processors’ caches. Hardware and programming languages that expose these weakly or un-synchronized memory accesses are said to have weak memory models. The lack of synchronization in weak memory models goes directly against the assumption of sequential consistency which still sits at the heart of most verification works. Concretely, we show how to perform verification in weak memory models using an existing program logic framework, Iris, that was traditionally limited to sequential consistency. In building on Iris, we inherit its mechanized proof of soundness of the core logic as well as the ability to perform mechanized program verification.

Secondly, we propose to bring the benefits of dependent types to the process of writing and automating proofs in the Rocq proof assistant. This aims to adress the limitations of Rocq's oldest — and, for a long time, only — tactic language: Ltac. Ltac's pitfalls are numerous and it is arguably unable to fulfill the requirements of large verification projects. Our contribution is a new tactic language called Mtac2. Mtac2 is based on Mtac, a principled metaprogramming language for Rocq offering strongly typed primitives based on Rocq’s own dependent type system. Mtac’s primitives could already be used to implement some tactics but it lacks the ability to directly interact with Rocq’s proof state and to perform backwards reasoning on it. Mtac2 extends Mtac with support for backwards reasoning and keeps in line with Mtac’s tradition of strong types by introducing the concept of typed tactics. Typed tactics statically track the expected type of the current goal(s) and can rule out entire classes of mistakes that often plague Ltac tactics.

The modern datacentres that power the cloud use virtualised infrastructures to improve efficiency through sharing, but I/O datapaths resist consolidation and remain a source of inefficiency. In response, shared network datapaths have emerged as an approach to reduce overheads and improve utilisation of communication heavy applications by multiplexing resources and better absorbing bursts. The problem is that sharing leads to contention in multiplexed cores and causes performance interference between tenants. Furthermore, shared datapaths are rigid and tenants depend on network protocols implemented by the operators, foregoing opportunities for running specialised protocols due to the safety and performance interference risks from untrusted tenant code. For my dissertation, I propose a time protection mechanism that uses time based accounting and enforcement to prevent performance interference and guarantee tail latency isolation at microsecond scale. I also propose a programmable datapath substrate that exposes a programming interface that safely enables tenants to upload custom network protocols to a shared datapath, so they can specialise protocols to applications. Finally, these mechanisms are combined in a shared network stack that integrates with the virtualised infrastructure of modern datacentres and provides microsecond scale latencies.

As users are exposed to an unprecedented range of security threats, a rich ecosystem of support mechanisms has emerged to assist the "last line of defense". Yet as these mechanisms become widely adopted in industry, a question arises: do they provide the support users actually need? In the first part of this talk, I will show that this is not always the case. Using phishing (one of the most prevalent and damaging cybercrimes) as a case study, I will present results from large-scale, real-world measurement studies that challenge common assumptions: that widely deployed mechanisms such as training and password managers are inherently effective, and that users primarily lack knowledge about this threat and how to detect it. Instead, I will show that phishing susceptibility is often an attention problem, due to limited and poorly surfaced indicators and cues. In the second part of the talk, I will discuss how we translate these insights into the design of novel systems that better support secure behavior. I will present a tailored countermeasure that assists users at critical decision points, and discuss its limitations in terms of increased user burden to introduce recent work on automating security decisions through AI-driven assistance. I will conclude by outlining key research challenges in designing security systems that are adaptive, context-aware, and robust.

Real-world AI systems must be robust across a wide range of conditions. One path to such robustness is if a model recovers a coherent structural understanding of its domain. But it is unclear how to measure, or even define, structural understanding. This talk will present theoretically-grounded definitions and metrics that test the structural recovery — or implicit "world models" — of generative models. We will propose different ways to formalize the concept of a world model, develop tests based on these notions, and apply them across domains. In applications ranging from testing whether LLMs apply logic to whether foundation models acquire Newtonian mechanics, we will see that models can make highly accurate predictions with incoherent world models. We will also connect these tests to a broader agenda of building generative models that are robust across downstream uses, incorporating ideas from statistics and the behavioral sciences. Developing reliable inferences about model behavior across tasks offer new ways to assess and improve the efficacy of generative models.

Online platforms increasingly rely on opaque content recommendation systems to curate personalized content. The black-box nature of these systems has raised significant societal concerns, such as formation of filter bubbles or promotion of extreme content. In response, regulatory bodies such as the European Commission have enacted digital regulations aimed at strengthening platform accountability and transparency. Achieving these goals requires audits of content recommendations and the mechanisms that govern them. To systematically audit personalized content recommendation systems deployed by online platforms, in this thesis we investigate their data gathering practices and transparency efforts. To this end, this thesis makes the following three contributions: First, it investigates personal data collection practices of online platforms, as these practices directly enable personalized content recommendations. Second, by employing sockpuppet accounts, it conducts an audit of transparency efforts implemented by online platforms through studying explanations provided for organic content recommendations. Finally, this thesis contributes to improving transparency in the procedures and objectives of recommendation systems deployed by online platforms.

Algorithmic problems in infinite groups arise naturally in the analysis of computational models, and they forge a fundamental link between algebra, logic, and computation. The central aim of my research is to understand the boundary between decidability and undecidability in computational algebra and group theory. Despite significant advances in the past 80 years, essential questions on the nature of these boundaries remain largely unanswered. The decision problems that we consider (the Diophantine Problem, membership problems, intersection problems) are particularly relevant to algorithmic verification, automata theory, and program analysis. Our methodology relates algorithms in groups to other central problems in infinite state systems, first-order arithmetic theories, and computer algebra. In this talk, I will illustrate a few recent results that expand the known decidability frontier, as well as some immediate and impactful open problems.

AI is reshaping software development, yet this rapid adoption risks introducing a new generation of security debt. In this talk, I will present my research program aimed at transforming AI from a source of vulnerabilities to a security enabler. I will begin by introducing a systematic framework for quantifying AI-induced cybersecurity risks through two benchmarks: CyberGym, which evaluates AI agents’ offensive capabilities in vulnerability reproduction and discovery, and BaxBench, which measures LLMs’ propensity to introduce security flaws when generating code. Building on these findings, I will present a secure-by-design approach for AI-generated code. This includes security-centric fine-tuning that embeds secure coding practices directly into models, as well as a decoding-time constraining mechanism based on type systems to enforce safety guarantees. Finally, I will conclude by discussing my future research on building broader security and trust in AI-driven software ecosystems.