Weak memory consistency models capture the outcomes of concurrent programs that appear in practice and yet cannot be explained by thread interleavings. Such outcomes pose two major challenges to formal methods.  First, establishing that a memory model satisfies its intended properties (e.g., supports a certain compilation scheme) is extremely error-prone: most proposed language models were initially broken and required multiple iterations to achieve soundness.  Second, weak memory models make verification of concurrent programs much harder, as a result of which there are no scalable verification techniques beyond a few that target very simple models.

In this talk, I present solutions to both of these problems. First, I show that the relevant meta-theory of weak memory models can be effectively decided (sparing years of manual proof efforts), and present Kater, a tool that can answer such queries in a matter of seconds.  Second, I present GenMC, the first  scalable stateless model checker that is parametric in the choice of the memory model, often improving the prior state of the art by orders of magnitude.

Distributed message-passing systems are both widespread and challenging to design and implement. Combining concurrency, asynchrony, and message buffering makes the verification problem algorithmically undecidable. We consider a top-down approach to this problem: one starts with a global communication protocol and automatically generates local specifications for its participants. The problem remains challenging because participants only obtain partial information about an execution through the messages they receive, which can cause confusion and undesired behaviours. The implementability problem asks if a (global) protocol can be implemented locally. It has been studied from two perspectives. On the one hand, multiparty session types (MSTs), with global types to specify protocols, provide an incomplete type-theoretic approach that is very efficient but restricts the expressiveness of protocols. On the other hand, high-level message sequence charts (HMSCs) do not impose any restrictions on the protocols, yielding undecidability of the implementability problem for HMSCs.   The work in this dissertation is the first to formally build a bridge between the world of MSTs and HMSCs. It presents a generalised MST projection operator for sender-driven choice. This allows a sender to send to different receivers when branching, which is crucial to handle common communication patterns from distributed computing. Nevertheless, the classical MST projection approach is inherently incomplete. Using our formal encoding from global types to HMSCs, we prove decidability of the implementability problem for global types with sender-driven choice. Furthermore, we develop the first direct and complete projection operator for global types with sender-driven choice, using automata-theoretic techniques, and show its effectiveness with a prototype implementation. Last, we introduce protocol state machines (PSMs) - an automata-based protocol specification formalism - that subsume both global types from MSTs and HMSCs with regard to expressivity. We use transformations on PSMs to show that many of the syntactic restrictions of global types are not restrictive in terms of protocol expressivity. We prove that the implementability problem for PSMs with mixed choice, which requires no dedicated sender for a branch but solely all labels to be distinct, is undecidable in general. With our results on expressivity, this shows undecidability of the implementability problem for mixed-choice global types.

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.

Decision support systems for classification tasks are predominantly designed to predict the value of the ground truth labels.  However, these systems also need to make human experts understand when and how to use these predictions to update their own  predictions. Unfortunately, this has been proven challenging. In this talk, I will introduce an alternative type of decision support systems  that circumvent this challenge by design. Rather than providing a single label prediction, these systems provide a set of label prediction  values, namely a prediction set, and forcefully ask experts to predict a label value from the prediction set. Moreover, I will discuss how to use conformal prediction, online learning and counterfactual inference to efficiently construct prediction sets that optimize experts’ performance,  provably. Further, I will present the results of a large-scale human subject study, which show that, for decision support systems based on  prediction sets, limiting experts’ level of agency leads to greater performance than allowing experts to always exercise their own agency.

Formal verification is a promising technique to ensure the reliability of low-level programs like operating systems and hypervisors, since it can show the absence of whole classes of bugs and prevent critical vulnerabilities. To realize the full potential of formal verification for real-world low-level programs, however one has to overcome several challenges, including: (1) dealing with the complexities of realistic models of real-world programming languages; (2) ensuring the trustworthiness of the verification, ideally by providing foundational proofs (i.e., proofs that can be checked by a general-purpose proof assistant); and (3) minimizing the manual effort required for verification by providing a high degree of automation.

This dissertation presents multiple projects that advance formal verification along these three axes: RefinedC provides the first approach for verifying C code that combines foundational proofs with a high degree of automation via a novel refinement and ownership type system. Islaris shows how to scale verification of assembly code to realistic models of modern instruction set architectures-in particular, Armv8-A and RISC-V. DimSum develops a decentralized approach for reasoning about programs that consist of components written in multiple different languages (e.g., assembly and C), as is common for low-level programs. RefinedC and Islaris rest on Lithium, a novel proof engine for separation logic that combines automation with foundational proofs.

The goal of under-approximating logics, such as incorrectness logic, is to reason about the existence of bugs  by specifying a subset of possible program behaviour. While this approach allows for the specification of a broad range of bugs, it does not account for divergence bugs (such as infinite loops), since the nature of the triple itself does not allow statements about infinite execution traces.     To fill this gap, I will present a divergent variant of the forward under-approximating (FUA) triple. This new separation logic reasons functionally compositionally about divergence bugs and is under-approximating in the sense that all specified bugs are true bugs, that is, reachable. It can detect divergence originating from loops, recursive function calls and goto-cycles.     I will motivate the talk by defining the type of divergent programs we are aiming to reason about, and show how previously introduced logics fall short of specifying their divergent behaviour. After introducing the FUA triple, I will outline how this triple differs from traditional over-approximating  and under-approximating approaches such as (partial) Hoare logic and incorrectness logic. Finally, I will discuss the mechanisms within the FUX framework that enable reasoning about divergence, with a focus on how to prove divergence arising from goto-cycles.

--

Please contact the office team for the Zoom link details.