Smart contract languages are increasingly popular and numerous, and their programming models and challenges are somewhat unusual. The ubiquitous presence of untrusted external code in such a system makes classical contracts unsuitable for safety verification, while the intentional presence of (potentially-mutating) callbacks via unknown code makes standard static analysis techniques imprecise in general. On the other hand, smart contract languages such as Vyper (for Ethereum) tightly encapsulate direct access to the program's state. In this talk I'll present a methodology for expressing contracts for this language, in a way that supports sound verification of safety properties, with deductive verification tooling (converting Vyper to Viper) to automate the corresponding proofs.

Based on joint work with Christian Bräm, Marco Eilers, Peter Müller and Robin Sierra; see also the accompanying paper at OOPSLA 2021. --- Please contact Office for Zoom link information.

The earliest paintings depicting a human date back to the Stone Age. Since that, sensing devices have been improved and nowadays, digital sensing can be found in everyone’s home. Nonetheless, the main element in many image compositions still is the human, i.e. most of the images one finds in the media, such as on the Internet or in textbooks and magazines, contain humans as the main point of attention. Since sensing of humans became more accurate, automated, affordable, and most importantly digital, it comes along with many opportunities in downstream applications such as telepresence, AR/VR, and health care, to only name a few. At the same time, this development also introduces major challenges, since raw sensing measurements cannot be immediately processed by those applications. Instead, it requires algorithms, which are capable of automatically analyzing human-related information and even synthesizing new content. In this talk, I will present some of our recent methods on the analysis and synthesis (rendering) of humans from digital measurements on the basis of Graphics, Vision, and Machine Learning concepts.

Language models that have been trained to predict the next word over billions of text documents have been shown to also significantly predict brain recordings of people comprehending language. Understanding the reasons behind the observed similarities between language in machines and language in the brain can lead to more insight into both systems. In this talk, we will discuss a series of recent works that make progress towards this question along different dimensions. The unifying principle among these works that allows us to make scientific claims about why one black box (language model) aligns with another black box (the human brain) is our ability to make specific perturbations in the language model and observe their effect on the alignment with the brain. Building on this approach, these works reveal that the observed alignment is due to more than next-word prediction and word-level semantics and is partially related to joint processing of select linguistic information in both systems. Furthermore, we find that the brain alignment can be improved by training a language model to summarize narratives. Taken together, these works make progress towards determining the sufficient and necessary conditions under which language in machines aligns with language in the brain.

Cryptography provides the data protection mechanisms that underlie security and privacy in the modern connected world. Given this pivotal role, implementations of cryptographic code must not only be correct, but also meet stringent performance and security requirements. Achieving these aims is often difficult and requires significant investment in software development and manual tuning.

This talk presents two approaches for automating the task of generating correct, secure, and efficient cryptographic code. The first, Rosita, uses a power consumption emulator to detect unintended leaky interactions between values in the microarchitecture. It then rewrites the code to eliminate these interactions and produce code that is resistant to power analysis. The second, CryptOpt, uses evolutionary computation to search for the most efficient constant-time implementation of a cryptographic function. It then formally verifies that the produced implementation is semantically equivalent to the original code.

Rosita is a joint work with Lejla Batina, Łukasz Chmielewski, Francesco Regazzoni, Niels Samwel, Madura A. Shelton, and Markus Wagner.CryptOpt is a joint work with Adam Chlipala, Chitchanok Chuengsatiansup, Owen Conoly, Andres Erbsen, Daniel Genkin, Jason Gross, Joel Kuepper, Chuyue Sun, Samuel Tian, Markus Wagner, and David Wu.

Please contact office for zoom link information.

String matching algorithms are everywhere. You use them every day, perhaps even without noticing. Whenever your mail client filters out spam, whenever your spell checker flags a spelling mistake, whenever your search engine of choice presents you with results it deems useful, to list just some examples. For many applications, we need more than finding exact occurrences of a pattern string in a text. Hence, in this talk, I consider the classical problem of finding parts of a text that are close to a given pattern string.

In particular, I consider the problem of finding all parts of a given text that can be transformed to a given pattern string by inserting, deleting, or substituting at most k characters—the Approximate String Matching problem. The first algorithms for this problem were developed in the 1970s, some of them are relevant even today. After a long line of research, around the year 2000, the progress in obtaining faster algorithms for Approximate String Matching came to a halt—even though the interest did not fade.

In a recent series of papers, I and coauthors improved the more than 20-year-old state-of-the-art algorithms. In this talk, I highlight the new tools and techniques that we developed for Approximate String Matching. Further, I give an overview of additional applications of our techniques to settings where text and pattern are given in a compressed setting or where we allow text and pattern to change dynamically.

The vast amount of digital data we create and collect has revolutionized many scientific fields and industrial sectors. Yet, despite our success in harnessing this transformative power of data, computational and societal trends emerging from the current practices of data science necessitate upgrading our toolkit for data analysis. In this talk, we discuss how practical considerations such as privacy and memory limits affect statistical inference tasks. In particular, we focus on two examples: First, we consider hypothesis testing with privacy constraints. More specifically, how one can design an algorithm that tests whether two data features are independent or correlated with a nearly-optimal number of data points while preserving the privacy of the individuals participating in the data set. Second, we study the problem of entropy estimation of a distribution by streaming over i.i.d. samples from it. We determine how bounded memory affects the number of samples we need to solve this problem. Please contact office for zoom link information