We build secure software on a seemingly obvious assumption: the processor executes instructions correctly and enforces the boundaries between programs, operating systems, and virtual machines. But what if the CPU itself breaks these rules? Over the past decade, research has found increasingly powerful ways in which processors violate the abstractions on which software relies. What started with tiny timing differences revealing secrets led to attacks such as Spectre and Meltdown, and more recently to CPU bugs that can directly corrupt data, bypass isolation, or expose information across security boundaries.

In this talk, I will show how seemingly harmless implementation details and useful optimizations turn into practical security vulnerabilities. Using examples from our research across Intel, AMD, and RISC-V processors, I will talk about how we discover and understand CPU vulnerabilities and ultimately turn them into security problems. The broader lesson goes beyond processor security: abstractions are only as strong as the layers implementing them. If we want trustworthy computer systems, hardware must increasingly be tested, analyzed, and secured with the same rigor that we already apply to software.

Anomaly detection is one of the fundamental topics in machine learning and artificial intelligence. The aim is to identify instances that deviate from the norm, so-called anomalies. Such anomalies arise in many scenarios, ranging from attacks on computer or energy networks to critical faults in industrial systems or rare tumors in medical imaging data. In this talk, I will first provide an overview of the field of anomaly detection, with an emphasis on approaches based on deep neural networks. I will then present recent algorithms and theoretical advances in deep anomaly detection. In particular, I will discuss why certain methods work and how their behavior can be better understood using principled analysis. Furthermore, I will highlight recent developments in anomaly detection for time series data, including new benchmark datasets and theoretically-grounded evaluation metrics. Finally, I will conclude with an outlook on promising future research directions in anomaly detection.

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.

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.

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.

AI systems increasingly reshape our networks, markets, and platforms. When deployed in social environments— online platforms, labor markets, and information ecosystems—AI interacts with complex human behavior, strategic incentives, and structural inequality. This talk focuses on foundational challenges and opportunities for AI systems: how to design and evaluate algorithmic interventions in complex social environments. I will present recent work on causal inference under competing treatments, which formalizes how competition for user attention and strategic behavior among experimenters distort experimental data and invalidate naïve estimates of algorithmic impact. By modeling experimentation as a strategic data acquisition problem, we show how evaluation itself becomes an optimization problem, and we derive mechanisms that recover meaningful estimates despite interference and competition. I connect this problem to deriving foundational properties of systems that enable reliable experimentation. Beyond this case study, the talk highlights broader implications for the design and evaluation of AI systems in networks, markets, and platforms. I argue that responsible deployment requires rethinking evaluation methodologies to account for incentives, feedback loops, and system-level effects, and I outline directions for how algorithmic and statistical tools can tackle these challenges.

Programmable hardware accelerator design is often driven by expert intuition and proxy metrics, with ground-truth feedback arriving only after costly RTL development, synthesis, and system integration.This weak feedback loop makes it difficult to compare alternatives, to understand which design choicesmatter, and to reason about feasibility, cost, and end-to-end performance in a principled way. This thesisargues for an executable, feasibility-first design methodology: designers should be able to (i) rapidly ruleout designs that cannot support the workloads of interest, (ii) obtain synthesis-backed cost metrics, and (iii)evaluate realistic end-to-end performance in a full system context, enabling systematic exploration beyondproxy-driven reasoning. As a concrete and demanding case study, we focus on reconfigurable programmable packet-processingpipelines, whose many architectural knobs strongly affect both capability (which programs can execute)and performance under strict line-rate and latency constraints. The thesis first contributes Kugelblitz, a nframework that decouples programs from architectures, performs fast feasibility checking, automaticallygenerates synthesizable RTL for feasible designs, and evaluates cost (area/timing) and system-level per-formance via cycle-accurate full-system simulation (SimBricks). Building on this foundation, we proposeFlamma sôlis, an automated exploration layer that searches the ConfigIR design space to optimize a user-chosen objective under user-chosen constraints. Flamma sôlis will automate design-space exploration by combining multi-stage evaluation with practical systems optimizations: it progressively applies increasingly expensive checks for feasibility, cost, and end-to-end performance, while using early termination, caching, and parallel execution to keep exploration tractable under realistic time budgets. We expect this approach to make architectural trade-offs explicit, reduce reliance on misleading proxies, and automate the discovery

Modern cryptography must navigate the transition to post-quantum security while meeting the demands of real-world systems. Due to the tension between post-quantum security and performance, this transition entails complex challenges on several fronts. In this talk, I will discuss the intricacies of provable security and how to establish solid theory for cryptographic building blocks that underpin our digital society. First, I will briefly cover my past work on searchable encryption and zero-knowledge proofs. In the main part of the talk, I will highlight my research on tools for advanced authentication in a post-quantum world. In particular, I will present my recent works on threshold signatures and blind signatures and discuss how to achieve stronger security guarantees under weak assumptions. In the end, I will highlight some open problems that are urgent to solve.

Today's ML workloads require networks that connect tens to hundreds of thousands of GPUs. Existing GPU clusters rely on network designs offering any-to-any connectivity while remaining agnostic to the data they carry. These traits are carried over from legacy CPU datacenters, limiting scalability and hindering GPU utilization. I will present workload-aware networking, a systematic approach that exploits structures inherent to machine learning traffic to co-design networks with ML workloads. I start by showing that large language model (LLM)’s network traffic exhibits a surprising property: it stays within the bottom layer of a switched network. This insight enables rail-only network designs that dramatically reduce cost and complexity. I then discuss TopoOpt, which uses reconfigurable networks to adapt to the repetitive, predictable traffic patterns of ML training, delivering performance improvements over today's network designs. Finally, I show that understanding traffic content in the network unlocks new functionalities. I introduce Checkmate, a system that embeds checkpointing into the network through gradient replication, enabling per-iteration checkpointing with zero GPU overhead. I conclude with future directions for extending these principles to emerging workloads like agentic AI, and building orchestration frameworks that automate network-workload co-design.

Artificial Intelligence (AI) models now serve as core components to a range of mature applications but remain vulnerable to a wide spectrum of attacks. Yet, the research community has yet to develop systematic understanding of model vulnerability. In this talk, I approach uncovering the mechanics of model failure from two complementary perspectives: the design of attack techniques and the features models exploit. First, I introduce The Space of Adversarial Strategies, a robustness evaluation framework constructed through a decomposition and reformulation of current attacks. With this, I isolate the components that drive attack success and provide insights for future defenses. Motivated by the widespread failure observed, I then turn to the feature space, where I uncover differences in visual processing and the human visual system that explain failures in AI systems. My work reveals that textures, or repeated patterns, are a core mechanism for driving model generalization, yet are also a primary source of vulnerability. I present new methodologies to quantify a model’s bias toward texture, uncover learned associations between textures and objects, and identify textures in images. With this, I find that up to 90% of failures can be explained by mismatches in texture information, highlighting texture as an important, yet overlooked, influence in model robustness. I conclude by outlining future work for addressing trustworthiness issues in both classification and generative settings, with particular attention to (mis)alignment between biological and artificial intelligence.

Digital identity controls access to many everyday essentials, from getting paid to accessing banking and benefits, and sits in the critical path of modern security. Even end-to-end encrypted messaging depends on authentic cryptographic identity, i.e., a trustworthy way to learn the cryptographic keys needed to encrypt messages to the right person. In practice, centralized identity providers become both a single point of failure and a single point of control: they decide what assertions are supported, and their compromise or coercion enables targeted attacks that are hard to detect. Yet, many strong proposals assume new ecosystems or significant user effort – assumptions that don’t hold for the systems and users we have today.

My thesis is that it is possible to make identity infrastructure more private, secure, and transparent at scale while designing for existing user and ecosystem constraints. I’ll present two case studies across the identity lifecycle.

First, I’ll discuss key transparency for end-to-end encrypted messaging: how to make centralized key directories auditable so that even a compromised server cannot quietly swap keys for targeted users. I’ll show how this line of work evolved from formal privacy and history guarantees (SEEMless) to a billion-user architecture (Parakeet) built for real operational constraints (such as distributed storage and long time horizons), which now underpins the key transparency deployments in WhatsApp and Facebook Messenger.

Second, I’ll briefly describe credential bootstrapping with accountability (CanDID): a path to establishing privacy-preserving credentials from existing web sources without assuming a fully mature verifiable-credential ecosystem, while supporting practical requirements like revocation, recovery, and compliance checks.

I’ll close by highlighting ongoing work and open problems motivated by these systems and sketch a research agenda for building auditable and privacy-preserving infrastructure at internet scale, for identity and beyond.

Large language models have transformed how we interact with technology, but most deployed systems remain reactive and rely on static, one-size-fits-all alignment, limiting trust in real-world, high-stakes settings. This talk explores a path toward personalized, trustworthy AI assistants that can reason, continually adapt, and align with user values while remaining safe and socially appropriate. I will introduce Computer-Using Agents that combine GUI operations and code generation to efficiently complete real-world tasks, and present CoAct-1, a multi-agent system that coordinates planning and execution. I will then discuss SEA, a black-box auditing algorithm for uncovering LLM knowledge deficiencies and probing failure modes such as hallucination under limited query budgets. Next, I will present WildFeedback, a framework that learns in-situ user preferences from natural, multi-turn interactions, enabling continual personalization beyond lab-style preference data. Finally, I will highlight ongoing work on proactive social intelligence and culturally grounded evaluation, spanning intention understanding, reasoning consistency, and value-aligned collaboration. Together, these advances move us closer to AI systems that don’t just respond, but adapt responsibly and assist people in ways that are reliable, equitable, and context-aware.

Software usages grow much faster than computing hardware. Paradoxically, modern software systems make inefficient use of computing resources: decades of feature creep have made them too generic to perform well on any specific task. These decades of growth have also made systems fragile -- and frankly insecure, glued together from countless components of diverse origins, critical or confidential, buggy, risky, AI-generated, or otherwise untrustworthy. This talk will take the audience on a journey at the intersection of systems and security. I will give an overview of my past and present works applying isolation and specialization techniques to make systems more more trustworthy and more efficient (Unikraft, FlexOS, CHERIoT), demonstrating the shortcomings of these techniques and how to address them (CIVs, SoK), and getting these advances deployed to better the real world. I will conclude with a forward-looking perspective on my research and impact plans towards achieving this vision of more robust and efficient software systems.

Machine learning relies on its ability to generalize from limited data, yet a principled theoretical understanding of generalization remains incomplete. While binary classification is well understood in the classical PAC framework, even its natural extension to multiclass learning is substantially more challenging. In this talk, I will present recent progress in multiclass learning that characterizes when generalization is possible and how much data is required, resolving a long-standing open problem on extending the Vapnik–Chervonenkis (VC) dimension beyond the binary setting. I will then turn to complementary results on efficient learning via boosting. We extend boosting theory to multiclass classification, while maintaining computational and statistical efficiency even for unbounded label spaces. Lastly, I will discuss generalization in sequential learning settings, where a learner interacts with an environment over time. We introduce a new framework that subsumes classically studied settings (bandits and statistical queries) together with a combinatorial parameter that bounds the number of interactions required for learning.

In many neural networks, different parameter values can yield the same loss, often due to underlying symmetries in the parameter space. We introduce a general framework for continuous symmetries based on equivariance in activation functions, revealing a new set of nonlinear, data-dependent symmetries. Using these symmetries, we derive topological properties of the minima and identify conserved quantities in gradient flows. As a practical application of parameter space symmetries, we present an algorithm called symmetry teleportation, which leverages parameter symmetries to search loss level sets for points with desired properties. This approach leads to improvements in both convergence and generalization. We also discuss future work on foundational understanding of deep learning that reveals, characterizes, and leverages hidden structures to shape optimization and model behavior, enabling more efficient and interpretable AI systems.

It has been described as the most important problem whose decidability is still open: the Skolem Problem asks how to determine algorithmically whether a given integer linear recurrence sequence (such as the Fibonacci numbers) has a zero term. This deceptively simple question arises across a wide range of topics in computer science and mathematics, from program verification and automata theory to number theory and logic. This talk traces the history of the Skolem Problem: from the early 1930s to the current frontier of one of the most enduring open questions in computer science.

Wearable AI systems, such as display-free smartglasses and augmented reality (AR) devices, are emerging as a new paradigm of personal computing. However, they introduce novel privacy harms for both users and bystanders, relying on multimodal data that reveals people's identities, activities, and surroundings. In this talk, I demonstrate that by building wearable AI systems for adaptation – enabling users and systems to dynamically adjust interactions across contexts – we can mitigate privacy risks while supporting meaningful use. First, through co-design studies with AR and security & privacy researchers, I establish a design space of alternatives to traditional interactions that reduce data exposure while maintaining functionality. To embed this privacy mindset in designers’ workflows, I develop interactive tools for critically analyzing risks in their own applications. Finally, I investigate how to automatically balance user experience and privacy for wearable AI users and bystanders, proposing an optimization framework for system-driven "negotiations" of sensing capabilities. I conclude by discussing open challenges and future research towards this vision of privacy-adaptive wearable AI, from technical mechanisms to implications for policy and regulation.

Having a solid system evaluation under realistic workloads and environments is essential for datacenter network research. Modern datacenter systems are shaped by a wide range of factors - including hardware behavior, software components, and complex interactions between them - whose combined effects on end-to-end performance is often difficult to predict. However, evaluating such systems on physical testbeds is frequently infeasible due to scale, cost, limited experimental control, and the increasing reliance on specialized hardware that may be unavailable or still under development. As a result, researchers often turn to simulation. Existing simulators, however, typically focus on isolated components, such as network protocols, host architectures, or hardware RTL, making it challenging to conduct faithful end-to-end evaluations or to scale experiments to realistic datacenter sizes. The goal of this thesis is to provide researchers with practical and scalable tools and methodologies for conducting faithful end-to-end system evaluation targeting modern datacenters. To this end, this thesis is structured around three components. First, it introduced SimBricks, an end-to-end simulation framework that enables the modular composition of best-of-breed simulators, allowing unmodified hardware and software system implementations to be evaluated together within a single virtual testbed. Second, it presented SplitSim, a simulation framework designed to make large-scale end-to-end evaluation practical by supporting mixed-.delity simulation, controlled decomposition, and efficient resource utilization. Finally, the thesis will include a set of case studies that apply SplitSim to the evaluation of large-scale networked systems, demonstrating a concrete evaluation workflow and distilling lessons on navigating trade-offs between fidelity, scalability, and simulation cost.

Stateless model checking (SMC) verifies a concurrent program by systematically exploring its state space. To combat the state-space explosion problem, SMC is frequently combined with Dynamic Partial Order Reduction (DPOR), a technique that avoids exploring executions that are deemed equivalent to one another. Still, DPOR’s scalability is limited by the size of the input program.

This thesis improves scalability by (i) providing direct support for common coding patterns that would otherwise have to be handled inefficiently, and (ii) combining DPOR with other state-space reduction techniques. Key to our contributions is a DPOR framework that generalizes an existing state-of-the-art algorithm.

Recent advances in generative AI have demonstrated the power of scaling: large language and vision models trained on internet-scale data now exhibit remarkable capabilities in perception, generation, and reasoning. These successes have inspired growing interest in bringing foundation-model paradigms to robotics, with the goal of moving beyond task-specific autonomy in constrained environments toward general-purpose robots that can operate robustly in open-world settings. However, robotics fundamentally differs from language and vision. Robot learning cannot rely on passive internet data at scale, and collecting large-scale, high-quality embodied interaction data remains expensive and slow. As a result, simply scaling data and model parameters is insufficient. To build general-purpose and robust robotics foundation models, we must instead ask: how can robots learn more from less data—and continue to improve over time? In this talk, I argue that reasoning in the loop offers a promising path forward. Rather than treating reasoning as a downstream capability applied after learning, I show how reasoning can be integrated directly into the learning process itself. This enables robots to learn from structured feedback, temporal context, and failure, thereby compensating for data scarcity and improving generalization. I will present a unified research agenda along three axes. First, I introduce approaches for spatial reasoning, enabling robots to ground language in 3D space and reason about object relationships for precise manipulation. Second, I discuss temporal reasoning, focusing on memory-centric models that retain, query, and reason over past observations to support long-horizon, high-precision control. Third, I show how reasoning over failures allows robots to understand why actions fail and use that understanding to self-improve, increasing robustness without additional supervision. Together, these results reframe robotics foundation models as systems that learn through reasoning, closing the loop between perception, action, and structured inference to enable self-improving autonomy.

Human-AI teams are increasingly deployed across high-stakes domains such as medical diagnosis, content moderation, and recruitment. These teams strive to leverage the strengths of both human decision-makers and AI models, while mitigating their respective weaknesses. For instance, such hybrid systems can combine the efficiency and quality of AI-generated decisions with human experience and domain knowledge. Moreover, they can be free of statistical biases in AI models and cognitive biases inherent to human decision-making. The combined system's performance can hence surpass that of the human or the AI model in isolation, achieving human-AI complementarity.

Despite the prevalence of such hybrid teams, most existing approaches remain heuristic-driven, ignore human users and their error models, and hence fail to optimize the human-AI team performance. My thesis strives to close these gaps and fully unlock this potential for complementarity by (i) optimizing for human-AI collaboration, rather than model-centric performance—ensuring these models best support and complement human decision-makers who utilize them—and (ii) designing efficient post-processing algorithms that ensure fairness of high-stakes decisions made by these teams—thereby supporting people who are affected by such decisions.

Fixed points are a recurring theme in computer science and related fields: shortest paths, game equilibria, semantics and verification, social choice theory, or dynamical systems are only a few of many instances. Various fixed point theorems - e.g. the famous Kleene fixed point theorem - state that fixed points emerge as limits of suitably seeded fixed point iterations. 

I will showcase in this talk a purely algebraic way of reasoning about fixed points which we call the algebra of iterative constructions (AIC). It lead us to discover novel fixed point theorems as well as prove fully algebraically well-established ones (e.g. Kleene, Tarksi-Kantorovic, and k-induction). As for the novel fixed point theorems, we will (given a suitable setting) obtain a method that maps any point to two canonical corresponding fixed points of a function by way of a limit of some fixed point iteration.

Our algebra is mechanized in Isabelle/HOL. Isabelle's sledgehammer tool is able to find proofs of fixed point theorems fully automatically whereas sledgehammer is not able to find such proofs relying only on Isabelle’s standard libraries.

From the audience I would like to learn: Do you encounter fixed points or fixed point problems in your work? Do you perhaps work on algorithms for solving fixed point problems?

I look forward to talking to you!