I will present two recent joint works done with Arnaud Sangnier and Nathalie Sznajder. We study networks of processes that all execute the same finite protocol and communicate synchronously in two different ways: a process can broadcast one message to all other processes or send it to at most one other process. We study two coverability problems with a parameterised number of processes (state coverability and configuration coverability). It is already known that these problem are Ackermann-hard (and decidable) in the general case. This already holds when the processes communicate only by broadcasts. We show that when forbidding broadcasts, the two problems are EXPSPACE-complete. We also study a restriction on the protocol: a Wait-Only protocol has no state from which a process can send and receive messages. We show that without broadcasts, both problems are PTIME-complete in this restriction, and with broadcasts, state coverability is PTIME-complete and configuration coverability PSPACE-complete.

Modern machine learning (ML) has largely been driven by neural networks, delivering outstanding results not only in traditional ML applications, but also permeating into classical sciences solving open problems in physics, chemistry, and biology. This success came at a cost, as typical neural network architectures are inherently complex and their reasoning processes opaque. In domains where insights weigh more than prediction, such as modeling of systems biology, or in high-stakes decision making, such as healthcare and finance, the reasoning process of a neural network however needs to be transparent. Recently, the mechanistic interpretation of this reasoning process has gained significant attention, which is concerned with understanding the *internal reasoning process* of a network, including what information particular neurons respond to and how these specific neurons are organized into larger circuits. In this talk, I will (1) gently introduce the topic of mechanistic interpretability in machine learning, (2) show how to discover mechanistic circuits within a neural network, (3) discuss the relevance of mechanistic interpretability in real-world applications, and (4) discuss what is still missing in the field.

Declassification allows a programmer to purposfully reveal secret information. In my thesis, I will argue that treating higher-order programs explicitly and compositionally is important when dealing with declassification, and using purpose-built logical-relations semantics, we can reason about declassification in new ways while fully supporting higher-order programs. To support this claim, I will study two different styles of declassification and their semantics. In the first part of my thesis, I will show how to reason about where declassification, an intensional declassification policy, in the higher-order setting by adapting logical relations techniques developed for noninterference. This approach leads to the first compositional semantics for an intensional declassification policy in the higher-order setting. In the second part of my thesis, I turn towards a style of declassification that has already been more extensively studied in the higher-order setting using logical relation semantics: what declassification. I will present a new approach to what declassification in higher-order languages. Specifically, I will present a novel dependency analysis using a dependent type system and show that what-declassification guarantees can be obtained from this dependency analysis using logical relations semantics.

From finance and healthcare to criminal justice and transportation, various domains that require critical decisions, traditionally made by humans, have increasingly incorporated artificial intelligence (AI) systems into the decision making process. Despite unprecedented advances in AI capabilities, in most real-world contexts, AI systems do not make highly consequential decisions autonomously; instead, they operate in conjunction with a human decision maker. The promise of human-AI collaboration lies in the complementary strengths of each to lead to better decisions overall. In this thesis, I present contributions on multiple dimensions of AI-assisted decision making that range from technical methodologies to empirical findings. I start by focusing on ways that AI systems can support strategic reasoning—the ability of humans to make decisions based on expectations about others’ behavior—and I introduce algorithmic methods that support a human decision maker in allocating resources to a population of other (strategic) humans. Then, I switch focus to counterfactual reasoning—the ability to reflect on how different decisions could have led events of the past to turn out differently. In that context, I propose algorithmic methods to help a human decision maker improve their future decisions by highlighting specific past decisions that could have led to better outcomes and may serve as a good learning signal. I conclude the thesis by proposing a computational model based on counterfactual simulations to predict the extent to which people hold a human and an AI agent responsible for an outcome in cases where the two agents are working together towards a common goal. The performance of this model is evaluated through an experiment with human participants conducted online.

Deciding if two graphs are isomorphic, i.e., whether they are structurally identical, is a fundamental computational problem that has many important applications. Despite extensive efforts in the past decades, GI has remained one of only few natural problems contained in NP that are neither known to be NP-complete nor known to be contained in P. In 20216, Babai proved in a breakthrough result that GI can be solved in quasipolynomial time. In the first part of my talk, I will give an overview on recent developments on testing isomorphism. A closely related problem is that of determining the similarity between two graphs. Arguably, this problem is even more relevant for many applications such as machine learning tasks on graph-structured data. Natural approaches such as counting edge modifications required to turn one graph into the other are computationally intractable even on very restricted input graphs. As a result, various other methods have been proposed to measure similarity between graphs such as graph motif counts, i.e., measuring similarity based on counting certain patterns appearing in the graphs. In the second part of the talk, we will consider different ways of measuring similarity and discuss relations to standard heuristics for isomorphism testing that have been discovered in recent years.

Machine Learning (ML) models are now integral to many critical systems, from self-driving cars to aviation, where their reliability and safety are crucial. Validating that these models perform their intended functions without failure is essential to prevent catastrophic outcomes. This thesis introduces novel tools and approaches inspired by software testing to specify and fuzz ML models for their functional correctness. By leveraging fuzzing and metamorphic testing techniques, we address the challenges of generating test inputs and defining test oracles for ML models. We begin by focusing on sequential decision-making problems, developing techniques to test action policies for reliability. Our PI-fuzz framework identifies bugs by generating diverse test states and applying test oracles relying on metamorphic relations. We then formalize metamorphic relations as hyperproperties and show their generalization across diverse domains and ML models. This led to the development of NOMOS, a declarative, domain-agnostic specification language for expressing and testing these hyperproperties. NOMOS is shown to be effective in identifying property violations across various ML domains. Additionally, we extend NOMOS to support code translation models. We evaluate several state-of-the-art models against a range of hyperproperties, uncovering numerous violations. This work contributes to the field by providing a comprehensive framework for assessing the reliability and safety of ML models in various applications.

We are witnessing the introduction of "intelligent" autonomous systems in many tasks that were traditionally performed by humans. Examples of such systems include autonomous vehicles, surveillance drones, and robots in warehouses, to name only a few. Often, these systems are developed using data-driven algorithms that result in them being "black-box" models. However, for the widespread usage of black-box systems in safety-critical applications, it is imperative to develop adequate trust in their behavior.

Toward the goal of developing trust in intelligent systems, in this thesis, we propose techniques to (i) explain the behavior of these systems in a human-interpretable manner, and (ii) facilitate their verification through formal methods. We are particularly interested in explaining and formalizing the temporal behavior of these systems. To this end, we design several techniques to automatically learn temporal properties from observed executions of systems. We explore several different problem settings, such as learning from noisy data or from only positive data, and consider several popular logical formalisms such as Linear Temporal Logic (LTL), Metric Temporal Logic (MTL), and Property Specification Language (PSL). In my thesis defense, I will give an overview of the various problem settings and techniques used to handle them. Further, I will demonstrate some of the empirical results obtained from the prototype implementation of the learning techniques.

Reasoning about concurrency in a realistic, non-toy language like C/C++ or Rust, which encompasses many interweaving complex features, is very hard. Yet, realistic concurrency involves relaxed memory models, which are significantly harder to reason about than the simple, traditional concurrency model that is sequential consistency. To scale up verifications to realistic concurrency, we need a few ingredients: (1) strong but abstract reasoning principles so that we can avoid the too tedious details of the underlying concurrency model; (2) modular reasoning so that we can compose smaller verification results into larger ones; (3) reasoning extensibility so that we can derive new reasoning principles for both complex language features and algorithms without rebuilding our logic from scratch; and (4) machine-checked proofs so that we do not miss potential unsoundness in our verifications. With these ingredients in hand, a logic designer can flexibly accommodate the intricacy of relaxed memory features and the ingenuity of programmers who exploit those features. In this dissertation, I present how to develop strong, abstract, modular, extensible, and machine-checked separation logics for realistic relaxed memory concurrency in the Iris framework, using multiple layers of abstractions. I report two main applications of such logics: (i) the verification of the Rust type system with a relaxed memory model, where relaxed memory effects are encapsulated behind the safe interface of libraries and thus are not visible to clients, and (ii) the compositional specification and verification of relaxed memory libraries, in which relaxed memory effects are exposed to clients.

The question of how to scalably verify large, stateful programs is one of the oldest—and still unsolved—questions of computer science. Over the last two decades, considerable progress has been made toward this goal with the advent of separation logic, a verification technique designed for modularly reasoning about stateful programs. While the original separation logic was only geared at verifying imperative, pointer-manipulating programs, modern versions of separation logic have become an essential tool in the toolbox of the working semanticist for modelling programming languages and verifying programs.

With my thesis, I will present a line of work that focuses on the weak spots of modern separation logic. Concretely, in the context of the separation logic framework Iris, I will target two broader areas, *step-indexing* and *automation*. Step-indexing is a powerful technique for recursive definitions that is crucial for handling many of the more advanced features of modern languages. But if one does not closely follow the path laid out by its inventors, perfectly natural proof strategies turn into dead ends. Automation, on the other hand, is important for reducing the overhead of verification, which is all too often preventing verification from scaling to larger code bases.

Regarding step-indexing, the thesis will present two projects, Transfinite Iris and Later Credits. Transfinite Iris shows how to generalize step-indexing—which traditionally applies only to safety properties—to proving liveness properties. Later Credits leverage separation logic to develop an amortized form of step-indexing that enables more flexible proof patterns. Regarding automation, the thesis will present Quiver and, potentially, Daenerys. Quiver introduces a new form of guided specification inference to reduce the specification overhead of separation logic verification. Daenerys brings heap-dependent assertions— logic-level assertions containing program-level expressions—to separation logic. Unlike traditional separation-logic assertions about programs, these heap-dependent assertions validate first-order reasoning principles thus laying the groundwork for SMT-solver based automation.

I will begin by demoing and releasing an LLM-based assistant that allows scientists to convert their papers (with a simple drag and drop) into short podcasts for communicating their research to a general audience. While we built the tool, we can’t explain its unreasonable effectiveness, i.e., we don’t really understand why it works or when it might fail. So in the rest of the talk, I will present our investigations into some basic curiosity-driven questions about LLMs; specifically, how do LLMs receive, process, organize, store, and retrieve information. 

Our analysis is centered around engaging LLMs in two specific types of cognitive tasks: first, syntactically-rich (semantically-poor) tasks such as recognizing formal grammars, and next, semantically-rich (syntactically-poor) tasks such as answering factual knowledge questions about real-world entities. Using carefully designed experimental frameworks, we attempt to answer the following foundational questions: (a) how can we estimate what latent skills and knowledge a (pre-trained) LLM possesses? (b) (how) can we distinguish whether some LLM has learnt some training data by rote vs. by understanding? (c) what is the minimum amount of training data/costs needed for a (pre-trained) LLM to acquire a new skill or knowledge?  (d) when solving a task, is training over task examples better, worse, or similar to providing them as in-context demonstrations?

I will present some initial empirical results from experimenting with a number of large open-source language models and argue that our findings they have important implications for the privacy of training data (including potential for memorization), the reliability of generated outputs (including potential for hallucinations), and the robustness of LLM-based applications (including our podcast assistant for science communication). 

Low-level code written in languages like C forms the bedrock of most computer systems today. Establishing the correctness of this code is important for the safety and security of our systems. The gold standard for code correctness is foundational verification -- the construction of mathematical proofs of program correctness verified in a proof assistant like Coq. However, foundational verification of low-level code is a tedious task that has, so far, largely relied on adapting code to suit the constraints of the verification framework, e.g., the programming idioms that are supported.

In this talk, I will present RefinedC, a new Coq-based C verification framework that aims to address the above limitation. By design, RefinedC is foundational (all proofs are mechanically verified within Coq), extensible (it can be extended to support new program properties, programming idioms and even new languages) and automation-friendly. Time permitting, I will also discuss projects that extend RefinedC's capabilities to reason about code written in other low-level languages like assembly, and code written in more than one language.

(This talk is based on joint work with several other research groups, notably the group of Derek Dreyer at MPI-SWS.)

Large language models (LLMs) currently dominate AI. They exhibit impressive, often human-like, behavior across a wide range of linguistic and non-linguistic tasks. However, LLMs are the result of a combination of clever engineering and financial investment, rather than a result of rigorous scientific or theoretical study. Thus, very little is known about how or why LLMs exhibit the behaviors that they do. As a result, LLMs often seem mysterious and unpredictable. In this talk, I will discuss recent work which seeks to characterize the mechanisms that LLMs employ in terms of higher-level data structures and algorithms. Using results on a series of simple tasks, I will argue that LLMs are not as inscrutable as they seem, but rather make use of simple and often modular computational components to solve complex problems.

In cyber-physical systems research, a significant challenge is synthesizing reliable controllers that meet general temporal specifications. These controllers must offer formal guarantees against various sources of disturbances. Efficient formal controller design opens up numerous exciting applications across different domains, including the autonomous vehicle industry, energy systems, and healthcare. In this talk, I will discuss formal controller synthesis for three different classes of dynamical systems. First, I will address our contributions to improving the scalability of abstraction-based controller design methods for dynamical systems with continuous state spaces and bounded uncertainty. These contributions include: (1) a data-driven scheme for relaxing the requirement of having analytical model, (2) a neural abstraction method to lower memory requirements of both synthesis and deployment, and (3) a scalable method for solving reach-avoid problems for multi-agent systems. Second, I will briefly describe our contributions to time-bounded model checking for continuous-time Markov decision processes, specifically: (1) a conditional decidability result, and (2) a systematic method for improving the scalability of numerical approximation methods. Finally, I will briefly discuss our results related to the decidability of reachability-related problems for linear dynamical systems, which include: (1) a hardness result for point-to-point reachability of linear dynamical systems with hyper-rectangular control sets, and (2) decidability of pseudo-reachability for hyperplane target sets.

WHO describes antimicrobial resistance (AMR) as one of the top global public health and development threats, while the World Bank estimates its additional healthcare burden as US$ 1 trillion by 2050. One strategy to combat AMR is significantly speeding up and reducing the cost of discovering new antibiotics, particularly those existing in nature but evading all current attempts to find them. Surprisingly, computer scientists play an increasingly important role in this endeavor. Modern biotechnology allows us to amass vast amounts of data on natural antibiotics and their tiny producers. However, specialized software and algorithms are the key to unlocking this wealth of information and turning it into medically important discoveries.

In my talk, I will demonstrate how computer science methods, from classical graph and string algorithms to deep learning, help transform antibiotic discovery into a high-throughput technology and realize the promise of already collected and rapidly growing biological datasets. The particular focus will be on analyzing sequencing (strings over the DNA alphabet of {A, C, G, T} letters) and mass spectrometry data (two-dimensional arrays of floating point values). In both cases, we deal with noisy experimental data, often rely on heuristics to make the processing time reasonable, and finally, get biologically relevant findings suitable for verification by our wet-lab collaborators.

Packing problems are ubiquitous optimization problems in computer science, where the task is to pack some class of objects into some class of containers. Canonical examples of packing problems include Knapsack, Subset Sum, and Bin Packing, but also several graph problems can be expressed as packing problems.

Most packing problems are NP-hard, and thus are typically attacked by approximation algorithms and fixed-parameter tractability, the two most recognized algorithmic paradigms for dealing with NP-hardness in theoretical computer science. This talk surveys recent developments on these two perspectives for packing problems. More concretely, I will talk about the following flavours of packing:

- (packing in geometry): how to pack polygons on the plane. - (packing numbers): how to pack items into a knapsack to maximize the value. - (packing in vector addition systems): how to reach your destination without running out of gas and money.

Misinformation poses a growing threat to our society. It has a severe impact on public health by promoting fake cures or vaccine hesitancy, and it is used as a weapon during military conflicts to spread fear and distrust. Current natural language processing (NLP) fact-checking research focuses on identifying evidence and the veracity of a claim. People’s beliefs however often do not depend on the claim and the rational reasoning as such, but on credible content that makes the claim seem more reliable, such as scientific publications or visual content that was manipulated or stems from unrelated context. To combat misinformation we need to show (1) "Why was the claim believed to be true?", (2) "Why is the claim false?", (3) "Why is the alternative explanation correct?". In the talk, I will zoom into two critical aspects of such misinformation supported by credible though misleading content. First, I will present our efforts to dismantle misleading narratives based on fallacious interpretations of scientific publications. Second, I will show how we can use multimodal large language models to (1) detect misinformation based on visual content, (2) provide strong alternative explanations for the visual content.

Blockchains revolutionized centralized sectors like banking and finance by promoting decentralization and transparency. In a blockchain, information is transmitted through transactions issued by participants or applications. Miners crucially select, order, and validate pending transactions for block inclusion, prioritizing those with higher incentives or fees. The order in which transactions are included can impact the blockchain final state. Moreover, applications running on top of a blockchain often rely on governance protocols to decentralize the decision-making power to make changes to their core functionality. These changes can affect how participants interact with these applications. Since one token equals one vote, participants holding multiple tokens have a higher voting power to support or reject the proposed changes. The extent to which this voting power is distributed is questionable and if highly concentrated among a few holders can lead to governance attacks. In this thesis, we audit the Bitcoin and Ethereum blockchains to investigate the norms followed by miners in determining the transaction prioritization. We also audit decentralized governance protocols such as Compound to evaluate whether the voting power is fairly distributed among the participants. Our findings have significant implications for future developments of blockchains and decentralized applications.

Despite ML models' impressive performance, training and deploying them is currently a somewhat messy endeavor. But does it have to be? In this talk, I overview my work on making ML "predictably reliable"---enabling developers to know when their models will work, when they will fail, and why.

To begin, we use a case study of adversarial inputs to show that human intuition can be a poor predictor of how ML models operate. Motivated by this, we present a line of work that aims to develop a precise understanding of the ML pipeline, combining statistical tools with large-scale experiments to characterize the role of each individual design choice: from how to collect data, to what dataset to train on, to what learning algorithm to use.

The algorithmic task of constructing hierarchical representations of data has been studied by various communities over many decades. Their applications range from statistics and databases to the analysis of complex networks and, more recently, machine learning, where they have proven useful for understanding text, images, graphs and multi-relational data. The reason why hierarchical representations are so ubiquitous is that many data sets stemming from nature or society are organized according to a latent hierarchy. Furthermore, in contrast to "flat" clustering techniques, like k-means or k-median which cannot capture fine-grained relationships among points, hierarchical clustering reveals the structure of a data set at multiple levels of granularity simultaneously.

Despite of the plethora of applications, the theory behind hierarchical clustering is underdeveloped, and popular heuristics offer little formal guarantees. In this talk I will present my work on algorithms with near optimal quality guarantees; in fact, in certain cases the algorithms run in near linear time, bridging the gap between theory and practice. Finally, I will discuss how to incorporate domain specific knowledge, leading to semi-supervised hierarchical clustering, as opposed to the traditional view of hierarchical clustering as an unsupervised learning method.

Finite-precision programs, prevalent in embedded systems, scientific computing, and machine learning, inherently introduce numerical uncertainties stemming from noises in the inputs and finite-precision errors. Furthermore, implementing these programs on hardware necessitates a trade-off between accuracy and efficiency. Therefore, it is crucial to ensure that numerical uncertainties remain acceptably small and to optimize implementations for accurate results tailored to specific applications. Existing analysis and optimization techniques for finite-precision programs face challenges in scalability and applicability to real-world scenarios. In this work, we expand the individual capabilities of these techniques by capturing the impact of uncertain inputs on discrete decisions and roundoff errors, by scaling floating-point verification for larger programs, and by specializing optimization for feed-forward deep neural networks.

As learning algorithms become more and more capable, they are used to tackle an increasingly large spectrum of tasks. Their applications range from understanding images, speech and natural language to making socially impactful decisions, such as about people's eligibility for loans and jobs. Therefore, it is important to better understand both the consequences of algorithmic decisions as well as the mechanisms by which algorithms arrive at their outputs. Of particular interest in this regard are fairness when algorithmic decisions impact peoples lives, as well as the behavior of deep learning algorithms, the most powerful but also opaque type of learning algorithm.

To this end, this thesis makes two contributions: First, we study fairness in algorithmic decision making. At a conceptual level, we introduce a metric for measuring unfairness in algorithmic decisions based on inequality indices from the economics literature. We show that this metric can be used to decompose the overall unfairness for a given set of users into between- and within-subgroup components and highlight potential tradeoffs between them as well as between fairness and accuracy. At an empirical level, we demonstrate the necessity for studying fairness in algorithmically controlled systems by exposing the potential for discrimination that is enabled by Facebook's advertising platform. In this context, we demonstrate how advertisers can target ads to exclude users belonging to protected sensitive groups, a practice that is illegal in domains such as housing, employment and finance, and highlight the necessity for better mitigation methods.

The second contribution of this thesis is aimed at better understanding the mechanisms governing the behavior of deep learning algorithms. First, we study the role that invariance plays in learning useful representations. We show that the set of invariances possessed by representations is of critical importance in determining whether they are useful for downstream tasks, more important than many other factors commonly considered to determine transfer performance. Second, we investigate memorisation in large language models, which have recently become very popular. By training models to memorise random strings, we surface a rich and surprising set of dynamics during the memorisation process. We find that models undergo two phases during memorisation, that strings with lower entropy are harder to memorise, that the memorisation dynamics evolve during repeated memorisation and that models can recall tokens in random strings with only a very restricted amount of information.

Reward functions are central to reinforcement learning (RL) as they implicitly capture the optimal behavior of the learning agent. Since the behavioral policy of the RL agent is updated based on the provided reward signals, the choice of the reward function can have a very large impact on how fast the reinforcement learning algorithm converges. One of the most popular approaches to speed up the learning process is a method of reward design. Reward design is a technique that replaces original rewards with designed rewards to make the problem easier to learn. In our work, we propose different reward design strategies that guarantee the desired characteristics of the designed reward functions. In particular, we want our designed rewards to satisfy three main characteristics: Invariance i.e., Reward signals should capture desired behavior without reward bugs, Interpretability i.e., Reward signals should be easy to diagnose and verify, and Informativeness i.e., reward signals should lead to effective learning. The theoretical analysis and empirical evaluations across various RL tasks highlight the effectiveness of our proposed methods.

Please contact grad-office@mpi-sws.org for zoom details

Platforms, devices, and algorithms are increasingly weaponized to control and harass the most vulnerable among us. Some of these harms occur at the individual and interpersonal level: for example, abusers in intimate partner violence (IPV) use smartphones and social media to surveil and stalk their victims. Others are more subtle, at the level of social structure: for example, in organizations, workplace technologies can inadvertently scaffold exploitative labor practices. This talk will discuss my research (1) investigating these harms via online measurement studies, (2) building interventions to directly assist survivors with their security and privacy; and (3) instrumenting these interventions, to enable scientific research into new types of harms as attackers and technologies evolve. I will close by sharing my vision for centering inclusion and equity in digital safety, security and privacy, towards brighter technological futures for us all.

As cloud applications become increasingly event-driven, Function-as-a-Service (FaaS) is emerging as an important abstraction. FaaS allows tenants to state their application logic as stateless functions without managing the underlying infrastructure that runs and scales their applications.

FaaS providers ensure the confidentiality of tenants’ data, to a limited extent, by isolating function instances from one another. However, for performance considerations, the same degree of isolation does not apply to sequential requests activating the same function instance. This compromise can lead to confidentiality breaches since bugs in a function implementation or its dependencies may retain state and leak data across activations. Moreover, platform optimizations that assume function statelessness may introduce unexpected behavior if the function retains state, jeopardizing correctness.

This dissertation presents two complementary systems: Groundhog and CtxTainter. Groundhog is a black-box and programming-language-agnostic solution that enforces confidentiality by efficiently rolling back changes to a function’s state after each function activation, effectively enforcing statelessness by breaking all data flows at the request boundary. CtxTainter is a development-phase dynamic data flow analysis tool that detects data flows that violate the statelessness assumption and reports them to the developer for reviewing and fixing.

As ubiquitous AI becomes increasingly integrated into the smart devices that users use daily, the rise of extensive datafication, data surveillance, and monetized behavioral engineering is becoming increasingly noticeable. Sophisticated algorithms are utilized to perform in-depth analyses of people's data, dissecting it to evaluate personal characteristics, thereby making significant and impactful algorithmic decisions for them. In this evolving digital environment, smart devices are no longer just functional tools; they have become active agents in shaping experiences, transforming lives as algorithmic decisions are etching pathways for people's futures. This trend is particularly concerning for vulnerable groups such as children, young people, and other marginalized communities, who may be disproportionately affected by these technological advancements. My research in human-computer interaction focuses on reimagining these data-driven AI systems to better support user autonomy. To address these challenges, I develop tools and systems that empower users and communities, especially those most vulnerable, to control their own experiences and information directly. These include: 1) human-AI interaction tools that enhance user decision-making power, 2) AI literacy tools for a deeper, critical understanding of data-driven systems, and 3) the development of actionable strategies and frameworks for policymakers and industry leaders to ensure the ethical development and use of AI technologies.

Our experience of the world is mediated by a continuous feedback loop between motor activity and sensory stimuli. Manipulating these sensorimotor loops offers a powerful means to influence user experience. Such loops, updating in milliseconds, demand devices with higher temporal resolution than those typically used in conventional human-computer interaction (HCI). In this talk, I will show how tapping into sensorimotor loops with tactile feedback allows us to alter our experience of the physical world and our own bodily sensations. Additionally, I will discuss how we can go beyond simply augmenting experience to enhancing human expression through sensorimotor augmentation.

Modern robotic applications consist of a variety of robotic systems that work together to achieve complex tasks. Programming these applications draws from multiple fields of knowledge and typically involves low-level imperative programming languages that provide little to no support for abstraction or reasoning. We present a unifying programming model, ranging from automated controller synthesis for individual robots to a compositional reasoning framework for inter-robot coordination. We provide novel methods on the topics of control and planning of modular robots, making contributions in three main areas: controller synthesis, concurrent systems, and verification. Our method synthesizes control code for serial and parallel manipulators and leverages physical properties to synthesize sensing abilities. This allows us to determine parts of the system's state that previously remained unmeasured. Our synthesized controllers are robust; we are able to detect and isolate faulty parts of the system, find alternatives, and ensure continued operation. On the concurrent systems side, we deal with dynamic controllers affecting the physical state, geometric constraints on components, and synchronization between processes. We provide a programming model for robotics applications that consists of assemblies of robotic components together with a run-time and a verifier. Our model combines message-passing concurrent processes with motion primitives and explicit modeling of geometric frame shifts, allowing us to create composite robotic systems for performing tasks that are unachievable for individual systems. We provide a verification algorithm based on model checking and SMT solvers that statically verifies concurrency-related properties (e.g. absence of deadlocks) and geometric invariants (e.g. collision-free motions). Our method ensures that jointly executed actions at end-points are communication-safe and deadlock-free, providing a compositional verification methodology for assemblies of robotic components with respect to concurrency and dynamic invariants. Our results indicate the efficiency of our novel approach and provide the foundation of compositional reasoning of robotic systems.

Searching and exploring information online is integral to everyday life, shaping how we learn, work, and create. As the Web paradigm evolves to include foundational AI models and beyond, we are experiencing a shift in how we search and work. With this transformation in human-AI interaction, it is important to investigate how we might present the user with the right information in the right context, the right representation, and at the right time. In this talk, I will share how I have explored these questions in the context of complex critical information work (such as knowledge discovery, synthesis, and creativity). I present insights about user behaviors and challenges from mixed-method studies observing how people conduct this work using today’s tools. Then, I present novel AI-powered tools and techniques that augment these cognitive processes by mining rich contextual signals from unstructured user-generated artifacts. By deepening our understanding of human cognition and behavior and building tools that understand user contexts more meaningfully, I envision a future where human-AI interactions are more personalized, context-aware, cognitively-convivial, and truly collaborative.

Data is today generated on smart devices at the edge, shaping a decentralized data ecosystem comprising multiple data owners (clients) and a service provider (server). Clients interact with the server with their personal data for specific services, while the server performs analysis on the joint dataset. However, the sensitive nature of the involved data, coupled with inherent misalignment of incentives between clients and the server, breeds mutual distrust. Consequently, a key question arises: How to facilitate private data analytics within a decentralized data ecosystem, comprising multiple distrusting parties?

My research shows a way forward by designing systems that offer strong and provable privacy guarantees while preserving data functionality. I accomplish this by systematically exploring the synergy between cryptography and differential privacy, exposing their rich interconnections in both theory and practice. In this talk, I will focus on two systems, CryptE and EIFFeL, which enable privacy-preserving query analytics and machine learning, respectively.

We present a number of methods used by central banks and regulatory authorities to assess the stability of the financial system, including stress tests, network analysis of the interbank market and models of interbank contagion and fire sales, aiming to capture the dynamics similar to those observed during the 2008 financial crisis. We will discuss the key role of banks in the money creation process, how this relates to monetary aggregates and what the introduction of central bank digital currencies and their different implementation options may mean in this context.

--

Please contact the office team for link information

People use storytelling to persuade, to entertain, to inform, and to make sense of their experiences as a community—and as a form of self-disclosure, personal storytelling can strengthen social bonds, build trust, and support the storyteller’s health. But computational analysis of narratives faces challenges, including difficulty in defining stories, lack of annotated datasets, and need to generalize across diverse settings. In this talk, I’ll present work addressing these challenges that uses methods from natural language processing (NLP) to measure storytelling both across online communities and within specific social contexts. This work has implications for NLP methods for story detection, the literary field of narratology, cooperative work in online communities, and better healthcare support. As one part of my research in NLP and cultural analytics, it also highlights how NLP methods can be used creatively and reliably to study human experiences.

As the Internet's user base and criticality of online services continue to expand daily, powerful adversaries like Internet censors are increasingly monitoring and restricting Internet traffic. These adversaries, powered by advanced network technology, perform large-scale connection tampering attacks seeking to prevent users from accessing specific online content, compromising Internet availability and integrity. In recent years, we have witnessed recurring censorship events affecting Internet users globally, with far-reaching social, financial, and psychological consequences, making them important to study. However, characterizing tampering attacks at the global scale is an extremely challenging problem, given intentionally opaque practices by adversaries, varying tampering mechanisms and policies across networks, evolving environments, sparse ground truth, and safety risks in collecting data. In this talk, I will describe my research on building empirical methods to characterize connection tampering globally and investigate the network technology enabling tampering. First, I will introduce novel network measurement methods for locating and examining network devices that perform censorship. Next, I will describe a modular design for the Censored Planet Observatory that enables it to remotely and sustainably measure Internet censorship longitudinally in more than 200 countries. I will introduce time series analysis methods to detect key censorship events in longitudinal Censored Planet data, and reveal global censorship trends. Finally, I will describe exciting ongoing and future research directions, such as building intelligent measurement platforms.

Planetary health is an emerging field which recognizes the inextricable link between human health and the health of our planet. Our planet’s growing crises include biodiversity loss, with animal population sizes declining by an average of 70% since 1970, and maternal mortality, with 1 in 49 girls in low-income countries dying from complications in pregnancy or birth. Underlying these global challenges is the urgent need to effectively allocate scarce resources. My research develops data-driven AI decision-making methods to do so, overcoming the messy data ubiquitous in these settings. Here, I’ll present technical advances in stochastic bandits, robust reinforcement learning, and restless bandits, addressing research questions that emerge from my close collaboration with the public sector. I’ll also discuss bridging the gap from research and practice, including anti-poaching field tests in Cambodia, field visits in Belize and Uganda, and large-scale deployment with SMART conservation software.

In the past decade, we have begun grappling with difficult questions related to the rise of AI, including: What rights do individuals have in the age of AI? When should we regulate AI and when should we abstain? What degree of transparency is needed to monitor AI systems? These questions are all concerned with AI accountability: determining who owes responsibility and to whom in the age of AI. In this talk, I will discuss the two main components of AI accountability, then illustrate them through a case study on social media. Within the context of social media, I will focus on how social media platforms filter (or curate) the content that users see. I will review several methods for auditing social media, drawing from concepts and tools in hypothesis testing, causal inference, and LLMs.

Living in a computer-reliant era, we’re balancing the power of computer systems with the challenges of ensuring their functional correctness and security. Program analysis has proven successful in addressing these issues by predicting the behavior of a system when executed. However, the complexity of conducting program analysis significantly arises as modern applications employ advanced, high-level programming languages and progressively embody the structure of a composite of independent modules that interact in sophisticated manners. In this talk, I will detail how to apply programming language theory to construct refined vulnerability specifications and reduce the complexity of program analysis across computational, conformational, and compositional aspects: - My primary focus will be on introducing some formal specifications that I have developed for modeling the common exponential worst-case computational complexity inherent in modern programming languages. These specifications have guided the first worst-case polynomial solution for detecting performance bugs in regexes. - I will also briefly discuss why generating inputs with complex conformation to target deep-seated bugs is a significant obstacle for existing techniques, and how I devised strategies to generate more sound input by intentionally satisfying previously unrecognized forms of dependencies. - Finally, as part of a vision to enhance security analysis in modern distributed systems, where different operations can be composed in a complex way and may interleave with each other, I will briefly discuss my efforts to establish new security notions to identify non-atomic operations in smart contracts and deter any potential attacks that might exploit their interactions.

Establishing strong guarantees for security-critical systems has never been more challenging. On the one hand, systems become increasingly complex and intricate. On the other hand, many security requirements are relational, i.e., they compare several execution traces. Examples are noninterference properties, program indistinguishability, and even algorithmic fairness. Due to their relational nature, formal reasoning about such properties quickly blows up in complexity. In this talk, I discuss the necessity to scale relational reasoning to larger software and black-box systems and present two of our recent contributions to tackle this challenge. In the first part, I focus on formal algorithms for white-box systems and show how to combine relational reasoning with non-relational specifications to enable the synthesis of smart contract control flows. In the second part, I focus on relational testing of black-box systems and illustrate its use in modeling and detecting microarchitectural information leakage in modern CPUs.

Linear dynamical systems (LDS) are mathematical models widely used in engineering and science to describe systems that evolve over time. In this thesis, we study algorithms for various decision problems of discrete-time linear dynamical systems. Our main focus is the Model-Checking Problem, which is to decide, given a linear dynamical system and an ω-regular specification, whether the trajectory of the LDS satisfies the specification. Using tools from various mathematical disciplines, most notably algebraic number theory, Diophantine approximation, automata theory, and combinatorics on words, we prove decidability of the Model-Checking Problem for large classes of linear dynamical systems and ω regular properties. We further exploit deep connections between linear dynamical systems and contemporary number theory to show that improving any of our decidability results would amount to major mathematical breakthroughs. Our results delineate the boundaries of decision problems of linear dynamical systems that, at the present time, can be solved algorithmically.

We need reliable measurement in order to develop rigorous knowledge about ML models and the systems in which they are embedded. But reliable measurement is a really hard problem, touching on issues of reproducibility, scalability, uncertainty quantification, epistemology, and more. In this talk, I will discuss the criteria needed to take reliability seriously — criteria for designing meaningful metrics, and for methodologies that ensure that we can dependably and efficiently measure these metrics at scale and in practice. I will give two examples of my research that put these criteria into practice: (1) large-scale evaluation of training-data memorization in large language models, and (2) evaluating latent arbitrariness in algorithmic fairness binary classification contexts. Throughout this discussion, I will emphasize how important it is to make metrics understandable for other stakeholders in order to facilitate public governance. For this reason, my work aims to design metrics that are legally cognizable — a goal that frames the both my ML and legal scholarship. I will draw on important connections that I have uncovered between ML and law: connections between (1) the generative-AI supply chain and US copyright law, and (2) ML arbitrariness and arbitrariness in legal rules. This talk reflects joint work with collaborators at The GenLaw Center, Cornell CS, Cornell Law School, Google DeepMind, and Microsoft Research.

In recent decades, the volume of sequential data processed in genomics and other disciplines has exploded. This trend escalates the challenge of designing text indexes – concise data structures that allow answering various queries efficiently. For example, pattern-matching queries ask if the text (a long string modeling the dataset) contains an occurrence of a given pattern (a short string provided at query time). The suffix array is a classic index for pattern matching and many other queries, but modern applications demand space-efficient alternatives like the FM index. Still, even these data structures struggle with massive highly repetitive datasets, such as human genome collections. This scenario requires indexes whose size is comparable to the best text compression methods.

The talk will introduce two tools originating from my text indexing research. Substring complexity is a well-behaved measure of text repetitiveness that aids in comparing the performance of compression algorithms. String synchronizing sets enable consistent selection of small subsets of text substrings. Recently, these tools became the core of the asymptotically smallest compressed text index with suffix-array functionality. Furthermore, they find applications beyond text indexing: in combinatorics on words, quantum string algorithms, and more.

Despite the remarkable progress in large language models (LLMs), it is well-known that natural language processing (NLP) models tend to fit for spurious correlations, which can lead to unstable behavior under domain shifts or adversarial attacks. In my research, I develop a causal framework for robust and fair NLP, which investigates the alignment of the causality of human decision-making and model decision-making mechanisms. Under this framework, I develop a suite of stress tests for NLP models across various tasks, such as text classification, natural language inference, and math reasoning; and I propose to enhance robustness by aligning model learning direction with the underlying data generating direction. Using this causal inference framework, I also test the validity of causal and logical reasoning in models, with implications for fighting misinformation, and also extend the impact of NLP by applying it to analyze the causality behind social phenomena important for our society, such as causal analysis of policies, and measuring gender bias in our society. Together, I develop a roadmap towards socially responsible NLP by ensuring the reliability of models, and broadcasting its impact to various social applications.

Advancements in Artificial Intelligence (AI) are impacting our lives, raising concerns related to data collection, and social alignment to the resilience of AI models. A major criticism of AI development is the lack of transparency in design and decision-making about AI behavior, potentially leading to adverse outcomes such as discrimination, lack of inclusivity and representation, breaching legal rules, and privacy and security risks. Underserved populations, in particular, can be disproportionately affected by these design decisions. Conventional approaches in soliciting people’s input, such as interviews, surveys, and focus groups, have limitations, such as often lacking consensus, coordination, and regular engagement. In this talk, I will present two examples of sociotechnical interventions for democratic and ethical AI. First, to address the need for ethical dataset creation for AI development, I will present a novel method "BivPriv," drawing ideas from accessible computing and computer vision in creating an inclusive private visual dataset with blind users as contributors. Then I will discuss my more recent work on "Inclusive.AI" funded by OpenAI to address concerns of social alignment by facilitating a democratic platform with decentralized governance mechanisms for scalable user interaction and integrity in the decision-making processes related to AI.

Today, nearly all internet connections are established using a cryptographic key exchange protocol. Fo r these protocols, we want to guarantee security even if an adversary can control the protocol’s execution or secr ets are leaked. A security analysis takes this into account and provides a mathematical proof relying on computati onal problems that are believed to be hard to solve. In this talk, I will first give an overview of the security p roperties of authenticated key exchange protocols and how to achieve them using cryptographic building blocks. I w ill talk about tight security and the role of idealized models such as the generic group model. In addition to cla ssical Diffie-Hellman based key exchange, I will also present recent results on isogeny-based key exchange, a prom ising candidate for post-quantum secure cryptography. Finally, I will touch upon examples of advanced cryptographi c primitives like ratcheted key exchange for secure messaging.

Machine learning security is an emerging area with many open questions lacking systematic analysis. In this talk, I will present three new algorithmic tools to address this gap: (1) algebraic proofs; (2) causal reasoning; and (3) sound statistical verification. Algebraic proofs provide the first conceptual mechanism to resolve intellectual property disputes over training data. I show that stochastic gradient descent, the de-facto training procedure for modern neural networks, is a collision-resistant computation under precise definitions. These results open up connections to lattices, which are mathematical tools used for cryptography presently. I will also briefly mention my efforts to analyze causes of empirical privacy attacks and defenses using causal models, and to devise statistical verification procedures with ‘probably approximately correct’ (PAC)-style soundness guarantees.

People around the world use data-driven online services every day. However, data center attacks and data breaches have become a regular and rising phenomenon. How, then, can one reap the benefits of data-driven statistical insights without compromising the privacy of individuals' data? In this talk, I will first present an overview of three disparate approaches towards privacy-preserving computations today, namely homomorphic cryptography, distributed trust, and secure hardware. These ostensibly unconnected approaches have one unifying element: oblivious algorithms. I will discuss the relevance and pervasiveness of oblivious algorithms in all the different models for privacy-preserving computations. Finally, I highlight the performance and security challenges in deploying such privacy-preserving solutions, and present three of my works that mitigate these obstacles through the design of novel efficient oblivious algorithms.

Third-party web tracking has been used to collect and analyze user browsing behavior, which has raised concerns about privacy among Internet users. In this talk, I will describe the mechanisms behind third-party web tracking and offer suggestions for user protection. My discussion will extend to our recent work on Personally Identifiable Information (PII) leakage-based tracking across various scenarios. I will conclude the talk by suggesting potential research directions to enhance transparency on the World Wide Web.