In order to improve performance or conserve energy, modern hardware implementations have adopted weak memory models; that is, models of concurrency that allow more outcomes than the classic sequentially consistent (SC) model of execution. Modern programming languages similarly provide their own language-level memory models, which strive to allow all the behaviors allowed by the various hardware-level memory models, as well as those that can occur as a result of desired compiler optimizations.

As these weak memory models are often rather intricate, it can be difficult for programmers to keep track of all the possible behaviors of their programs. It is therefore very useful to have an abstraction layer over the model that can be used to ensure program correctness without reasoning about the underlying memory model. Program logics are a way of constructing such an abstraction—one can use their syntactic rules to reason about programs, without needing to understand the messy details of the memory model for which the logic has been proven sound.

Unfortunately, most of the work on formal verification in general, and program logics in particular, has so far assumed the SC model of execution. This means that new logics for weak memory have to be developed.

This thesis presents two such logics—fenced separation logic (FSL) and weak separation logic (Weasel)—which are sound for reasoning under two different weak memory models.

FSL considers the C/C++ concurrency memory model, supporting several of its advanced features. The soundness of FSL depends crucially on a specific strengthening of the model which eliminates a certain class of undesired behaviors (so-called out-of-thin-air behaviors) that were inadvertently allowed by the original C/C++ model.

Weasel works under weaker assumptions than FSL, considering a model which takes a more fine-grained approach to the out-of-thin-air problem. Weasel's focus is on exploring the programming constructs directly related to out-of-thin-air behaviors, and is therefore significantly less feature-rich than FSL.

Using FSL and Weasel, the thesis explores the key challenges in reasoning under weak memory models, and what effect different solutions to the out-of-thin-air problem have on such reasoning. It explains which reasoning principles are preserved when moving from a stronger to a weaker model, and develops novel proof techniques to establish soundness of logics under weaker models.

Congruence closure of ground equations is a fundamental operation used in numerous applications in computer science. Going back to the early 1960's, this operation was considered critical in recognizing common subexpressions for optimizing compilers especially for high performance computing. In the 80's, it was used to combine decision procedures for various quantifier-free theories in building verification systems. More recently, it serves as a glue in fast decision procedures based on the satisfiability modulo theory framework. In 1997, an approach for generating congruence closure of uninterpreted symbols was proposed by generating a canonical rewrite system on constants by abstracting nonconstant subterms in ground equations. This framework is not only time and space efficient, but generates canonical forms with respect to the congruence closure relation. Algorithms based on this have been integrated well into SMT solvers. This talk will discuss how semantic properties of function symbols, including commutativity, idempotency, nilpotency and identity, as well as associative-commutative can also be considered without having to need any sophisticated machinery, such as associative-commutative unification, associated compatible termination orderings and associative-commutative completion, typically needed for generating canonical rewrite systems of ground equations with asssocative-commutative function symbols. The use of semantic congruence closure for generating uniform interpolants if they exist will be shown; interpolants have been found useful for automatically generating loop invariants of programs.

In the past, information and knowledge dissemination was relegated to brick-and-mortar classrooms, newspapers, radio, and television. As these processes were simple and centralized, the models behind them were well understood and so were the empirical methods for optimizing them. In today’s world, the internet and social media have become a powerful tool for information and knowledge dissemination: Wikipedia gets more than 1 million edits per day, Stack Overflow has more than 17 million questions, 25% of the US population visits Yahoo! News for articles and discussions, Twitter has more than 60 million active monthly users, and Duolingo has 25 million users learning languages online. These developments have introduced a paradigm shift in the process of dissemination. Not only has the nature of the task moved from being centralized to decentralized, but the developments have also blurred the boundary between the creator and the consumer of the content, i.e., information and knowledge. These changes have made it necessary to develop new models to understand the dissemination process and to develop new methods to optimize it.

At a broad level, we can view the participation of users in the process of dissemination as falling into one of two settings: collaborative or competitive. In the collaborative setting, the participants work together in crafting knowledge online, e.g., by asking questions and contributing answers,or by discussing news or opinion pieces. In contrast, as competitors, they vie for the attention of their followers on social media. This thesis investigates both these settings.

The first part of the thesis focuses on the understanding and analysis of content being created online collaboratively. To this end, I propose models for understanding the complexity of the content of collaborative online discussions by looking exclusively at the signals of agreement and disagreement expressed by the crowd. This leads to a formal notion of complexity of opinions and online discussions. Next, I turn my attention to the participants of the crowd, i.e., the creators and consumers themselves, and propose an intuitive model for both the evolution of their expertise and the value of the content they collaboratively contribute and learn from on online Q&A based forums. The second part of the thesis explores the competitive setting. It provides methods to help creators gain more attention from their followers on social media. In particular, I consider the problem of controlling the timing of the posts of users with the aim of maximizing the attention that their posts receive under the idealized setting of full-knowledge of timing of posts of others. To solve it, I develop a general reinforcement learning based method which is shown to have good performance on the when-to-post problem and which can be employed in many other settings as well, e.g., determining the reviewing times for spaced repetition which lead to optimal learning. The last part of the thesis looks at methods for relaxing the idealized assumption of full knowledge. This basic question of determining the visibility of one’s posts on the followers’ feeds becomes difficult to answer on the internet when constantly observing the feeds of all the followers becomes unscalable. I explore the relationship between this problem and the well-studied problem of web-crawling to update a search engine’s index and provide algorithms with performance guarantees for feed observation policies that minimize the error in the estimate of the visibility of one’s posts.

In supervised machine learning, in an abstract sense, a concept in a given reference class has to be inferred from a small set of labeled examples. Machine teaching refers to the inverse problem, namely the problem to compress any concept in the reference class to a "teaching set" of labeled examples in a way that the concept can be reconstructed. The goal is to minimize the worst-case teaching set size taken over all concepts in the reference class, while at the same time adhering to certain conditions that disallow unfair collusion between the teacher and the learner. Applications of machine teaching include multi-agent systems and program synthesis. In this presentation, it is first shown how preference relations over concepts can be used in order to guarantee collusion-free teaching and learning. Intuitive examples are presented in which quite natural preference relations result in data-efficient collusion-free teaching of complex classes of concepts. Further, it is demonstrated that optimal collusion-free teaching cannot always be attained by the preference-based approach. Finally, we will challenge the standard notion of collusion-freeness and show that a more stringent notion characterizes teaching with the preference-based approach. This presentation summarizes joint work with Shaun Fallat, Ziyuan Gao, David G. Kirkpatrick, Christoph Ries, Hans U. Simon, and Abolghasem Soltani.

Abstract: Support for hardware acceleration and parallel software workloads on heterogeneous multiprocessor platforms is becoming increasingly relevant in the design of high-performance and power-efficient real-time embedded systems. Communication between jobs dispatched on different cores and specialized hardware accelerators such as FPGAs and GPUs is most often implemented using asynchronous events. The delays incurred by each task due to the time spent waiting for such events should appropriately be accounted for in the timing analysis of the resulting scheduling behavior. This talk presents the event-driven delay-induced (EDD) task model, which is suitable to represent and analyze the timing behavior of complex computing workloads that incur event-related delays in the communication and synchronization between different processing elements. The EDD task model generalizes several existing task models, providing enhanced expressiveness towards the timing analysis of parallel processing workloads that involve both synchronous and asynchronous hardware acceleration requests. Two analysis techniques for EDD tasks executing on single-core platforms under fixed-priority scheduling are presented; then, a model transformation technique is provided to analyze parallel real-time tasks executing under partitioned multiprocessor scheduling by means of a set of EDD tasks. In the experiments, partitioned scheduling of parallel tasks is shown to outperform federated scheduling when the proposed analysis approach is combined with specialized partitioning heuristics.

Please contact the office team for link information.

There are dozens or perhaps hundreds of papers that claim that some data release that was thought to protect privacy does not. This has led to a widespread belief that anonymized data is easily attacked. As a result, organizations may stop releasing certain valuable data (Netflix recommendations, certain statistics on genetic studies), or apply strong anonymization that reduces the utility of the data (US Census Bureau, Facebook URLs dataset). In this broadly accessible talk, I will argue that most data anonymity attack papers don't measure privacy correctly, leading to conclusions that are at best invalid, and often very misleading. I will describe a more appropriate measure that we have used in the past in our anonymity bounty program. This is work in progress.

Enzian is a research computer built at ETH Zurich which combines a server-class CPU with a large FPGA in an asymmetric 2-socket NUMA system. It is designed to be used individually or in a cluster to explore the design space for future hardware and its implications for system software. Enzian is deliberately over-engineered, and (as I'll show) can replicate the use-cases of almost all other FPGA platforms used in academic research today. Perhaps unique to Enzian is exposing the CPU's native cache-coherence protocol to applications on the FPGA, and I'll discuss the additional opportunities this offers for research as well as the challenges we faced in interoperating with an existing coherence protocol not designed for this use-case. There are nine Enzian systems operational so far, being used locally at ETH and remotely by collaborators.

---

Please contact the MPI-SWS Office Team for the ZOOM link information. .

We introduce Concurrent NetKAT (CNetKAT), an extension of the network programming language NetKAT with multiple packets and with operators to specify and reason about concurrency and state in a network We provide a model of the language based on partially ordered multisets, well-established mathematical structures in the denotational semantics of concurrent languages. We prove that CNetKAT is a sound and complete axiomatization of this model, and we illustrate the use of CNetKAT through various examples. More generally, CNetKAT is analgebraic framework to reason about programs with both local and global state. In our model these are, respectively, the packets and the global variable store, but the scope of applications is much more general, including reasoning about hardware pipelines inside an SDN switch. This is joint work with Jana Wagemaker, Nate Foster, Tobia Kappe, Dexter Kozen, and Jurriaan Rot.

Please contact the office team for link information,

While steady progress has been made in visual perception, the performance is mainly benchmarked under fair weather/lighting conditions. Even the best-performing algorithms on the existing benchmarks can become untrustworthy in unseen domains or in adverse weather/lighting conditions. The ability to robustly cope with those conditions is absolutely essential for outdoor applications such as autonomous driving. In this talk, I will present our work on semantic scene understanding under adverse weather/illumination conditions and under general unseen domains. This covers multiple contributions: weather phenomenon simulation, curriculum domain adaptation, reference-guided learning, supervision fusion, sensor fusion, and supervision distillation. Our methods all contribute towards the goal of all-season perception and have achieved state-of-the-art performance for semantic scene understanding under bad weather/lighting conditions and under the synthetic2real cross-domain setting.

We present fully automated approaches to safety and termination analysis of probabilistic while-programs whose guards and expressions are polynomial expressions over random variables and parametrised distributions. We combine methods from symbolic summation and statistics to derive invariants as valid properties over higher-order moments, such as expected values or variances, of program variables, synthesizing this way quantitative invariants of probabilistic program loops. We further extend our moments-based analysis to prove termination of considered probabilistic while-programs. This is a joint work with Ezio Bartocci, Joost-Pieter Katoen, Marcel Moosbrugger and Miroslav Stankovic.

--

Please contact the MPI-SWS Office Team for the ZOOM link information.

Microarchitectural security is one of the most challenging and exciting problems in system security today. With the discovery of transient execution attacks, it has become clear that microarchitectural attacks have significant impact on the security properties of software running on a processor that runs code from various stakeholders (such as, for instance, in the cloud). This talk will first provide an overview of the current understanding of microarchitectural security, with a focus on how the research community has built formal models for processors that support proving that software is resilient to specific classes of microarchitectural attacks. Next, we turn to the problem of validating these proposed formal models: how can we convince ourselves and others that a given formal model is an adequate model for a given real-world processor, and that we can justifiably trust the security properties proven based on the model. This is an instance of the more general problem of empirically validating whether a real-world system satisfies the assumptions on which a formal model relies. We will discuss a small case study where we empirically validated a formally proven security property of a simple processor by systematically attacking the corresponding real-world implementation of the processor. We end with some conclusions and reflections on how our experiences from this case study might help us build more adequate formal models.

--

Please contact the MPI-SWS Office Team for the ZOOM link information.

This talk will introduce the emerging field of quantum computer vision. I will first review several recent methods for 3D reconstruction and 3D data analysis developed at the Visual Computing and Artificial Intelligence Department (with the collaboration of the 4D and Quantum Vision group), and then argue that several problem classes—especially those requiring combinatorial optimisation—can benefit from formulations involving quantum phenomena. Finally, we will see that modern adiabatic quantum annealers (AQA) allow solving real-world tasks and achieve state-of-the-art accuracy for such important problems as permutation synchronisation and non-rigid shape matching.

Thanks to the recent advances in AQA technology and the possibility to access the machines remotely, researchers from various fields of science can nowadays develop and test new quantum techniques on real quantum hardware. AQA are computing machines that can efficiently solve unconstrained binary optimisation problems using the principles postulated in the adiabatic theorem of quantum mechanics [Born and Fock, 1928; Kadowaki and Nishimori, 1998]. AQA perform a series of annealings, i.e., gradual transitions between the initial and final ("problem") Hamiltonians. They find global optima on non-convex energy landscapes using quantum fluctuations, quantum effects of qubit superposition and entanglement, as well as tunnelling through the energy landscape.

Rigorous approaches based on controller synthesis can generate correct-by-construction controllers that guarantee that the system under control meets some higher-level tasks. By reducing designing and testing cycles, synthesis can help create safe autonomous systems that involve complex interactions of dynamics and decision logic. In general, however, synthesis problems are known to have high computational complexity for high dimensional and nonlinear systems. In this talk, I will present a series of new synthesis algorithms that suggest that these challenges can be overcome and that rigorous approaches are indeed promising. I will talk about how to synthesize controllers for linear systems, nonlinear systems, hybrid systems with both discrete and continuous control variables, and multi-agent systems, with guarantees on the safety and optimality of the solutions.

Please contact the office team for link information.

Synthesizing photo-realistic images is of crucial importance for a large variety of applications, including movies, telepresence, design visualizations, or training simulators. New technologies such as virtual and augmented reality require high-quality renderings at high frame rates, which poses a tremendous challenge for the design of rendering algorithms. Traditionally, this challenge has been attacked either by simulating light transport from physical first principles, or by re-using existing images to create new views. In recent years, data-driven techniques have risen as a third pillar in the space of rendering algorithms. All approaches have their distinct pros and cons, giving rise to a continuum of hybrid algorithms trying to merge the best of the three worlds. In this talk, I will give an overview over this continuum, with an emphasis on our more recent work, which seeks to reconcile image quality, rendering efficiency, and controllability.

When using distributed machine learning (ML) systems to train models on a cluster of worker machines, users must configure a large number of parameters: hyper-parameters (e.g. the batch size and the learning rate) affect model convergence; system parameters (e.g. the number of workers and their communication topology) impact training performance. Some of these parameters, such as the number of workers, may also change in elastic machine learning scenarios. In current systems, adapting such parameters during training is ill-supported. In this talk, I will describe our recent work on KungFu, a distributed deep learning library for TensorFlow and PyTorch that is designed to enable adaptive and elastic training. KungFu allows users to express high-level Adaptation Policies (APs) that describe how to change hyper-and system parameters during training. APs take real-time monitored metrics (e.g. signal-to-noise ratios) as input and trigger control actions (e.g. cluster rescaling or synchronisation strategy updates). For execution, APs are translated into monitoring and control operators that are embedded in the dataflow graph. APs exploit an efficient asynchronous collective communication layer, which ensures concurrency and consistency of monitoring and adaptation operations.

--

Please contact the MPI-SWS Office Team for the ZOOM link information.

In this presentation, I will talk about some of the recent work we did on new methods for reconstructing computer graphics models of real world scenes from sparse or even monocular video data. These methods are based of bringing together neural network-based and explicit model-based approaches.

I will also talk about new neural rendering approaches that combine explicit model-based and neural network based concepts for image formation in new ways. They enable new means to synthesize highly realistic imagery and videos of real work scenes under user control.

Within a span of just a few years, we have gone from completely trusting our hardware to realising that everything is broken and all our security guarantees are built on sand. Memory chips have fundamental (Rowhammer) flaws that allow attackers to modify data without accessing it and CPUs are full of side channels and transient execution problems that lead to information leakage across pretty much all security boundaries. Combined, these issues have led to a string of high-profile attacks. In this talk, I will discuss some of the developments in such attacks, mostly by means of the attacks in which our group was involved. Although the research was exciting, I will argue that the way we conduct security research on hardware is broken. The problem is that the interests of hardware manufacturers and academics do not align and this is bad for everyone.

--

Please contact MPI-SWS Office Team for Zoom link information.

Domain-specific hardware accelerators for graphics, deep learning, image processing, and other tasks have become pervasive to meet the performance and energy-efficiency needs of emerging applications. However, such specializations are inherently at odds with the programmability long enjoyed by software developers from general-purpose processors. In this talk, I will explore the feasibility of programmable, domain-agnostic accelerators that can be morphed and instantiated to specialized accelerators at runtime through software. In particular, I will present Coarse-Grained Reconfigurable Array (CGRA) as a promising approach to offer high accelerator efficiency while supporting diverse tasks through compile-time configurability. The central challenge is efficient spatio-temporal mapping of the applications expressed in high-level programming languages with complex data dependencies, control flow, and memory accesses to the accelerator. We approach this challenge through a synergistic hardware-software co-designed approach with (a) innovations at the architecture level to improve the efficiency of the application execution as well as ease the burden on the compilation, and (b) innovations at the compiler level to fully exploit the architectural optimizations for quality and fast mapping. Finally, I will share systems-level considerations for real-world deployment of domain-agnostic accelerators in the context of edge computing.

Please contact the office team for link information

Over the last decade, the advent of social media has profoundly changed the way people produce and consume information online. On these platforms, users themselves play a role in selecting the sources from which they consume information, overthrowing traditional journalistic gatekeeping. Moreover, advertisers can target users with news stories using users’ personal data. This new model has many advantages: the propagation of news is faster, the number of news sources is large, and the topics covered are diverse. However, in this new model, users are often overloaded with redundant information, and they can get trapped in filter bubbles by consuming divisive and potentially false information. To tackle these concerns, in my thesis, I address the following important questions:

(i) How efficient are users at selecting their information sources? We have defined three intuitive notions of users’ efficiency in social media: link, in-flow, and delay efficiency. We use these three measures to assess how good users are at selecting who to follow within the social media system in order to most efficiently acquire information.

(ii) How can we break the filter bubbles that users get trapped in? Users on social media sites such as Twitter often get trapped in filter bubbles by being exposed to radical, highly partisan, or divisive information. To prevent users from getting trapped in filter bubbles, we propose an approach to inject diversity in users’ information consumption by identifying non-divisive, yet informative information.

(iii) How can we design an efficient framework for fact-checking? Proliferation of false information is a major problem in social media. To counter it, social media platforms typically rely on expert fact-checkers to detect false news. However, human fact-checkers can realistically only cover a tiny fraction of all stories. So it is important to automatically prioritize and select a small number of stories for human to fact check. However, the goals for prioritizing stories for fact-checking are unclear. We identify three desired objectives to prioritize news for fact-checking. These objectives are based on the users’ perception of truthfulness of stories. Our key finding is that these three objectives are incompatible in practice.

Algorithms are increasingly used to aid decision-making in high-stakes settings including employment, lending, healthcare, and the legal system. This development has led to an ecosystem of growing complexity in which algorithms and people interact around consequential decisions, often mediated by organizations and firms that may be in competition with one another.

We consider two related sets of issues that arise in this setting. First, concerns have been raised about the effects of algorithmic monoculture, in which multiple decision-makers all rely on the same algorithm. In a set of models drawing on minimal assumptions, we show that when competing decision-makers converge on the use of the same algorithm as part of a decision pipeline, the result can potentially be harmful for social welfare even when the algorithm is more accurate than any decision-maker acting on their own. Second, we consider some of the canonical ways in which data is simplified over the course of these decision-making pipelines, showing how this process of simplification can introduce sources of bias in ways that connect to principles from the psychology of stereotype formation.

The talk will be based on joint work with Sendhil Mullainathan and Manish Raghavan.

Please contact the office team for link information.

Real-number arithmetic is a key component in many domains like neural networks and embedded controllers, thus providing efficient and correct tooling is highly desirable. As real numbers are infinite, they are commonly represented using finite-precision arithmetic which makes computations efficient but this representation necessarily introduces errors into results. In safety-critical settings finite-precision programs must thus come with rigorous proofs about their behavior, and it is the compilers job to preserve these properties.

In general, compiler verification deals with exactly this task, proving that the compiler preserves properties of the input program throughout the compilation pipeline. As of today, the most-common formats of floating-point and fixed-point numbers are not well supported by state-of-the-art verified compilers.

In my thesis I want to improve the state-of-the-art support for finite-precision arithmetic for verified compilation of numerical kernels for floating-point and fixed-point arithmetic. For floating-point arithmetic, state-of-the-art verified compilers, support only simple direct mappings into assembly instructions.

In the thesis we develop a novel floating-point semantics that allows verified compilers to perform performance oriented optimizations of floating-point programs, and use this semantics to extend the verified compiler CakeML with support for real-number programs. Fixed-point arithmetic is not supported by major verified compilers.

For the remaining research work of the thesis, we suggest first an approach to for verified code generation for fixed-point arithmetic. As an alternative, we suggest an extension of a verified compiler with support for fixed-point arithmetic.

Financial applications such as Landing and Payment protocols, and their realization in decentralized financial (DeFi) applications in Blockchains, comprise a unique domain where bugs in the code may be exploited by anyone to steal assets. This situation provides unique opportunities for formal verification to enable "move fast and break nothing". Formal verification can be used to detect errors early in the development process and guarantee correctness when a new version of the code is deployed.

I will describe an attempt to automatically verify DeFis and identify potential bugs. The approach is based on breaking the verification of DeFis into decidable verification tasks. Each of these tasks is solved via a decision procedure which automatically generates a formal proof or a test input showing a violation of the specification. In order to overcome undecidability, high level properties are expressed as ghost states and static analysis used to infer how low level programs update ghost states.

--

Please contact MPI-SWS Office Team for Zoom link information

Want to speed up data access? Add a cache! Data caching, as the solution to performance woes, is as old as our field. However, we have been less aggressive at caching computation. While memoization is a widely known technique, it is rarely employed as pervasively as data caching. In this talk, I'll present examples of how we've used computational caching in areas ranging from interpretable machine learning to program synthesis to automatic parallelization.

--

Please contact the MPI-SWS office team for Zoom link details.

In the synthesis problem, we are given a specification over input and output signals, and we synthesize a system that realizes the specification: with every sequence of input signals, the system associates a sequence of output signals so that the generated computation satisfies the specification. The above classical formulation of the problem is Boolean. The talk surveys recent efforts to automatically synthesize reactive systems that are not only correct, but also of high quality. Indeed, designers would be willing to give up manual design only after being convinced that the automatic procedure that replaces it generates systems of comparable quality. We distinguish between behavioral quality, which refers to the way the specification is satisfied, and costs, which refer to resources that the system consumes. We argue that both are crucial for synthesis to become appealing in practice. __________________________________________________________________________

Please contact MPI-SWS Office Team for Zoom link information

Distributional reinforcement learning (RL) is a new approach to RL with the emphasis on the distribution of the rewards obtained rather than just the expected reward as in traditional RL. In this work we take the distributional point of view and analyse a number of sampling-based algorithms such as value iteration, TD(0) and policy iteration. These algorithms have been shown to converge under various assumptions but usually with completely different proofs. We have developed a new viewpoint which allows us to prove convergence using a uniform approach. The idea is based on couplings and on viewing the approximation algorithms as Markov processes in their own right. It originated from work on bisimulation metrics in which I have been working for the last quarter century. This is joint work with Philip Amortila (U. Illinois), Marc Bellemare (Google Brain) and Doina Precup (McGill, Mila and DeepMind).

Please contact MPI-SWS office for the Zoom links

Indisputably, the Web has revolutionized the way people receive, consume, and interact with information. At the same time, unfortunately, the Web offers a fertile ground for amplifying socio-technical issues like the spread of hateful content and false information; hence there is a pressing need to develop techniques and tools to understand, detect, and mitigate these issues on the Web. In this talk, I will present our data-driven quantitative approach towards understanding such emerging socio-technical problems, focusing on the spread of hateful content targeting specific demographic groups. Also, I will present our work on understanding mitigation strategies employed by social networks (i.e., moderation interventions) and assessing their effectiveness towards reducing the prevalence and impact of these issues on the Web.

Computational social choice is an interdisciplinary field that studies collective decision making from an algorithmic perspective. Determining the winners under various voting rules is a mainstream area of research in computational social choice. Many such rules assume that the voters provide complete information about their preferences, an assumption that is often unrealistic because typically only partial preference information is available.  This state of affairs has motivated the study of the notions of the necessary winners and the possible winners with respect to a variety of voting rules.

The main aim of this talk is to present an overview of winner determination under incomplete information and to highlight some recent advances in this area, including the development of a framework that aims to create bridges between computational social choice and data management. This framework infuses relational database context into social choice and allows for the formulation of sophisticated queries about voting rules, candidates, winners, issues, and positions on issues. We will introduce the necessary answer semantics and the possible answer semantics to queries and will explore the computational complexity of query evaluation under these semantics.

------------------------------------------------------------

Please contact MPI-SWS Office Team for Zoom link information

Program termination is a key question in program verification. This talk considers the termination of probabilistic programs, programs that can describe e.g., randomized algorithms, security algorithms and Bayesian learning.

Probabilistic termination has several nuances. Diverging program runs may occur with probability zero. Such programs are almost surely terminating (AST). If the expected duration until termination is finite, they are positive AST.

This talk presents a simple though powerful proof rule for deciding AST, reports on recent approaches towards automation, and sketches a Dijkstra-like weakest precondition calculus for proving positive AST in a compositional way.

-------------

Please contact MPI-SWS Office Team for Zoom link information

Cyber-physical systems (CPSs) combine cyber capabilities, such as computation or communication, with physical capabilities, such as motion or other physical processes. Cars, aircraft, and robots are prime examples, because they move physically in space in a way that is determined by discrete computerized control algorithms. Designing these algorithms is challenging due to their tight coupling with physical behavior, while it is vital that these algorithms be correct because we rely on them for safety-critical tasks.

This talk highlights some of the most fascinating aspects of the logical foundations for developing cyber-physical systems with the mathematical rigor that their safety-critical nature demands. The underlying logic, differential dynamic logic, provides an integrated specification and verification language for dynamical systems, such as hybrid systems that combine discrete transitions and continuous evolution along differential equations.

In addition to providing a strong theoretical foundation for CPS, differential dynamic logics have been instrumental in verifying many applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, automotive systems, mobile robot navigation, and a surgical robotic system for skull-base surgery. Logic is the foundation to provably transfer safety guarantees about models to CPS implementations. This technology is also the key ingredient behind Safe AI for CPS.

-------

Please contact MPI-SWS office team for zoom link information

An ever-increasing amount of data to be analyzed raises novel challenges for the theory of computation. How can we prove computational difficulty of a seemingly simple task when facing enormous data sets? Developing such methods is essential for determining which problems can or cannot be solved at a large scale.

Fine-grained complexity theory in P provides corresponding methods by establishing tight connections between fundamental algorithmic problems. In particular, we show that many natural sequence comparison problems cannot be solved in truly subquadratic time, assuming a stronger version of the famous P ≠ NP conjecture. These results give rigorous insights into the challenges encountered, e.g., in the context of genome comparison, and even aid in developing novel efficient algorithms.

Despite such early successes, this young theory is still in its infancy: In particular, most of the current results establish connections between isolated algorithmic problems, rather than between classes of problems. Can we establish a more encompassing theory and turn the current problem-centric state of the art to a full-fledged structural complexity theory for large data sets? Towards this end, we discuss a quest for completeness and classification theorems (inspired by a finite-model-theoretic approach and the Dichotomy Theorem for constraint satisfaction problems), and present promising initial results.

The Internet was meant to be neutral: treat all traffic the same, without discriminating in favor of specific apps, sites, or services. As commercial interests threaten this ideal, many countries have introduced neutrality regulations. Unfortunately, none of them are actually enforceable. In this talk, I will first discuss the challenge of inferring whether a network is neutral or not using solely external observations. Then, I will show that we can go beyond neutrality inference and reach network transparency, in which networks provide explicit hints that enable their users to reliably assess network behavior, including neutrality. Network transparency, however, requires exposing information about what traffic is seen where and when, which can hurt user privacy. I will close by looking at the important question of whether network transparency indeed must come at the cost of reduced anonymity for Internet users.

--

Please contact MPI-SWS Office Team for Zoom link information

Don't we all dream of the perfect assistant whom we can just tell what to do and the assistant can figure out how to accomplish the tasks? Formally, given a specification F(X,Y) over the set of input variables X and output variables Y, we want the assistant, aka functional synthesis engine, to design a function G such that (X,Y=G(X)) satisfies F. Functional synthesis has been studied for over 150 years, dating back Boole in 1850's and yet scalability remains a core challenge. Motivated by progress in machine learning, we design a new algorithmic framework Manthan, which views functional synthesis as a classification problem, relying on advances in constrained sampling for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification. On an extensive and rigorous evaluation over 609 benchmarks, we demonstrate that Manthan significantly improves upon the current state of the art, solving 356 benchmarks in comparison to 280, which is the most solved by a state of the art technique; thereby, we demonstrate an increase of 76 benchmarks over the current state of the art. The significant performance improvements, along with our detailed analysis, highlights several interesting avenues of future work at the intersection of machine learning, constrained sampling, and automated reasoning.

Please contact MPI-SWS office team for link information

We are seeing a persistent gap between the theoretical security of e.g. cryptographic algorithms and real world vulnerabilities, data-breaches and possible attacks. Software developers – despite being computer experts – are rarely security experts, and security and privacy are usually, at best, of secondary importance for them. They may not have training in security and privacy or even be aware of the possible implications, and they may be unable to allocate time or effort to ensure that security and privacy best practices and design principles are upheld for their end users. Understanding their education and mindsets, their processes, the tools that they use, and their pitfalls are the foundation for shifting development practices to be more secure. This talk will give an overview of security challenges for developers, and interdisciplinary research avenues to address these.

--

Please contact MPI-SWS Office team for link information.

To establish software security at scale, we need efficient automated vulnerability discovery techniques that can run on thousands of machines. In this talk, we will discuss the abundant opportunities and fundamental limitations of fuzzing, one of the most successful vulnerability discovery techniques. We will explore why only an exponential number of machines will allow us to discover software bugs at a linear rate. We will discuss the kind of correctness guarantees that we can expect from automatic vulnerability discovery, anywhere from formally proving the absence of bugs to statistical claims about program correctness. We shall touch upon unexpected connections to ecological biostatistics and information theory which allow us to address long-standing scientific and practical problems in automatic software testing. Finally, we will take a forward looking view and discuss our larger vision for the field of software security.

--

Please contact MPI-SWS Office for Zoom link information

Software is everywhere, and almost everywhere, software is broken. Some bugs just crash your printer; others hand an identity thief your bank account number; still others let nation-states spy on dissidents and persecute minorities. This talk outlines my work preventing bugs using a blend of programming languages techniques and systems design. First, I'll talk about securing massive, security-critical codebases without clean slate rewrites. This means rooting out hard-to-find bugs---as in Sys, which scales symbolic execution to find exploitable bugs in systems like the twenty-million line Chrome browser. It also means proving correctness of especially vulnerable pieces of code---as in VeRA, which automatically verifies part of the Firefox JavaScript engine. Finally, I'll discuss work on stronger foundations for new systems---as in CirC, a recent project unifying compiler infrastructure for program verification, cryptographic proofs, optimization problems, and more.

--

Please contact MPI-SWS Office for link information

Building intelligent visual systems is essential for the next generation of artificial intelligence systems. It is a fundamental tool for many disciplines and beneficial to various potential applications such as autonomous driving, robotics, surveillance, augmented reality, to name a few. An accurate and efficient intelligent visual system has a deep understanding of the scene, objects, and humans. It can automatically understand the surrounding scenes. In general, 2D images and 3D point clouds are the two most common data representations in our daily life. Designing powerful image understanding and point cloud processing systems are two pillars of visual intelligence, enabling the artificial intelligence systems to understand and interact with the current status of the environment automatically. In this talk, I will first present our efforts in designing modern neural systems for 2D image understanding, including high-accuracy and high-efficiency semantic parsing structures, and unified panoptic parsing architecture. Then, we go one step further to design neural systems for processing complex 3D scenes, including semantic-level and instance-level understanding. Further, we show our latest works for unified 2D-3D reasoning frameworks, which are fully based on self-attention mechanisms. In the end, the challenges, up-to-date progress, and promising future directions for building advanced intelligent visual systems will be discussed.

--

Please contact MPI-SWS office for link information.

Satisfying the growing demand for more compute as processor performance continues to stagnate in the post-Moore era requires radical changes throughout the systems stack. A proven strategy is to move from today’s general purpose platforms to post-Moore systems, specialized systems comprising tightly integrated and co-designed hardware and software components. Currently, designing and implementing these systems is a complex, laborious, and risky process, accessible to few and only practical for the most computing intensive applications. In this talk, I discuss the nascent challenges in building post-Moore systems and illustrate them through specific systems I have built. As a first step to address these challenges, I present Simbricks, a modular simulation framework that flexibly combines existing simulators for computers, custom hardware, and networks, into complete virtual post-Moore systems, enabling developers to compare and evaluate designs earlier and quicker. I conclude with a look towards future opportunities in abstractions, tooling, and methodology to further simplify the development of post-Moore systems.



Please contact MPI-SWS Office for link information.

In this talk, I will describe a distributionally robust learning framework that offers accurate uncertainty quantification and rigorous guarantees under data distribution shift. This framework yields appropriately conservative yet still accurate predictions to guide real-world decision-making and is easily integrated with modern deep learning. I will showcase the practicality of this framework in applications on agile robotic control and computer vision. I will also introduce a survey of other real-world applications that would benefit from this framework for future work.

--

Please contact MPI-SWS Office for Zoom link information

To create trustworthy AI systems, we must safeguard machine learning methods from catastrophic failures. For example, we must account for the uncertainty and guarantee the performance for safety-critical systems, like in autonomous driving and health care, before deploying them in the real world. A key challenge in such real-world applications is that the test cases are not well represented by the pre-collected training data. To properly leverage learning in such domains, we must go beyond the conventional learning paradigm of maximizing average prediction accuracy with generalization guarantees that rely on strong distributional relationships between training and test examples. In this talk, I will describe a distributionally robust learning framework that offers accurate uncertainty quantification and rigorous guarantees under data distribution shift. This framework yields appropriately conservative yet still accurate predictions to guide real-world decision-making and is easily integrated with modern deep learning. I will showcase the practicality of this framework in applications on agile robotic control and computer vision. I will also introduce a survey of other real-world applications that would benefit from this framework for future work.

--

Please contact MPI-SWS office team for Zoom link information

Despite the phenomenal empirical successes of deep learning in many application domains, its underlying mathematical mechanisms remain poorly understood. Mysteriously, deep neural networks in practice can often fit training data perfectly and generalize remarkably well to unseen test data, despite highly non-convex optimization landscapes and significant over-parameterization. Moreover, deep neural networks show extraordinary ability to perform representation learning: feature representation extracted from a trained neural network can be useful for other related tasks.

In this talk, I will present our recent progress on building the theoretical foundations of deep learning, by opening the black box of the interactions among data, model architecture, and training algorithm. First, I will show that gradient descent on deep linear neural networks induces an implicit regularization effect towards low rank, which explains the surprising generalization behavior of deep linear networks for the low-rank matrix completion problem. Next, turning to nonlinear deep neural networks, I will talk about a line of studies on wide neural networks, where by drawing a connection to the neural tangent kernels, we can answer various questions such as how training loss is minimized, why trained network can generalize, and why certain component in the network architecture is useful; we also use theoretical insights to design a new simple and effective method for training on noisily labeled datasets. Finally, I will analyze the statistical aspect of representation learning, and identify key data conditions that enable efficient use of training data, bypassing a known hurdle in the i.i.d. tasks setting.

--

Please contact the MPI-SWS office team for link information.

Failures of machine learning systems can threaten both the security and privacy of their users. My research studies these failures from an adversarial perspective, by building new attacks that highlight critical vulnerabilities in the machine learning pipeline, and designing new defenses that protect users against identified threats. In the first part of this talk, I'll explain why machine learning models are so vulnerable to adversarially chosen inputs. I'll show that many proposed defenses are ineffective and cannot protect models deployed in overtly adversarial settings, such as for content moderation on the Web. In the second part of the talk, I'll focus on the issue of data privacy in machine learning systems, and I'll demonstrate how to enhance privacy by combining techniques from cryptography, statistics, and computer security.

--

Please contact MPI-SWS Office for link information

Software bugs are pervasive and costly.  As a result, developers spend the majority of their time debugging their software.  Traditionally, debugging involves inspecting and tracking the runtime behavior of a program.  Alas, program inspection is computationally expensive, especially when employing powerful techniques such as dynamic information flow tracking, data-race detection, and data structure invariant checks.  Moreover, debugging logic is difficult to specify correctly.  Current tools (e.g., gdb, Intel Pin) allow developers to write debugging logic in an imperative inline programming model that mirrors the programming style of traditional software.  So, debugging logic faces the same challenges as traditional software, including concurrency, fault handling, dynamic memory, and extensibility.  In general, specifying debugging logic can be as difficult as writing the program being debugged!

In this talk, I will describe a new data-centric debugging framework that alleviates the performance and specification limitations of current debugging models.  The key idea is to use deterministic record and replay to treat a program execution as a massive data object consisting of all program states reached during the execution.  In this framework, developers can express common debugging tasks (e.g., tracking the value of a variable) and dynamic analyses (e.g., data-race detection) as queries over an execution's data object.  My research explores how a data-centric model enables large-scale parallelism to accelerate debugging queries (JetStream and SledgeHammer) and relational query models to simplify the specification of debugging logic (SledgeHammer and the OmniTable Query Model).

--

Please contact MPI-SWS office for Zoom link information

Conversations are central to our social systems. Understanding how conversationalists navigate through them could unlock great improvements in domains like public health, where the provision of social support is crucial. To this end, I develop computational frameworks that can capture and systematically examine aspects of conversations that are difficult, interesting and meaningful for conversationalists and the jobs they do. Importantly, these frameworks aim to yield actionable understandings—ones that reflect the choices that conversationalists make and their consequences, beyond the inert linguistic patterns that are produced in the interaction.

Please contact MPI-SWS Office for link information.

Graphs are widespread models for relations between entities. One of the fundamental problems when dealing with graphs is to decide isomorphism, i.e., to check whether two graphs are structurally identical. Even after decades of research, the quest for an efficient graph-isomorphism test still continues. In this talk, I will discuss the Weisfeiler-Leman (WL) algorithm as a powerful combinatorial procedure to approach the graph-isomorphism problem. The algorithm can be seen as a link between many research areas (the ""WL net""), including, for example, descriptive complexity theory, propositional proof complexity, and machine learning. I will present work regarding the two central parameters of the algorithm – its dimension and the number of iterations – and explore their connection to finite-model theory. I will also touch on some past and ongoing projects in other areas from the WL net.

--

Please contact MPI-SWS office team for link information.

Deep learning today is successful in almost any domain of computer vision. The talk will revisit the seminal work of FlowNet to show how deep learning was applied to optical flow and led to a paradigm shift in this domain. Optical flow, disparity, motion and depth boundaries as well as uncertainty estimation with multi-hypothesis networks will be covered and it will be discussed how deep learned models could surpass traditional methods. Asking the more fundamental question what models we need in computer vision, the talk will then progress to recent deep-learned scene representation approaches such as the ones obtained by learned signed distance functions and NeRF and provide a perspective on how computer vision might change in the future.

--

Please contact the MPI-SWS office team for link information.

The success of today's hardware and software systems is due in part to a mature toolbox of techniques, like abstraction, that systems designers use to manage complexity. While powerful, these techniques are also subtly dangerous: they induce implicit trust relationships among system components and between related systems, presenting attackers with many opportunities to undermine the integrity of our hardware and software. This talk discusses an approach to building systems with precise control over trust, drawing on techniques from theoretical computer science. Making this approach practical is a challenge that requires innovation across the entire technology stack, from hardware to theory. I will present several examples of such innovations from my research and describe a few potential directions for future work.

--

Please contact MPI-SWS Office Team for link information

Data is now everywhere: enormous amounts of data are produced and processed every day. Data is gathered,exchanged, and used extensively in computations that serve many purposes: e.g., computing statistics on populations, refining bidding strategies in ad auctions, improving recommendation systems, and making loan or hiring decisions. Yet, data is not always transacted and processed in a responsible manner. Data collection often happens without the data holders' consent, who may also not be compensated for their data. Privacy leaks are numerous, exhibiting a need for better privacy protections on personal and sensitive data. Data-driven machine learning and decision making algorithms have been shown to both mimic past bias and to introduce additional bias in their predictions, leading to inequalities and discrimination. In this talk, I will focus on my research on using data in a more responsible manner. The main focus of the talk will be on my work on the privacy issues that arise in data transactions and data-driven analysis, under the lens of a framework known as differential privacy. I will go over my work on designing transactions for data where we provide differential privacy guarantees to the individuals whose sensitive data we are buying and using in computations, and will focus on my recent work on providing differential privacy to agents in auction settings, where it is natural to want to protect the valuations and bids of said agents. I will also give a brief overview of the other directions that I have followed in my research, both on the optimization and economic challenges that arise when letting agents opt in and out of data sharing and compensating them sufficiently for their data contributions, and on how to reduce the disparate and discriminatory impact of data-driven decision-making.

--

Please contact MPI-SWS office team for Zoom link information

The network stack in today's operating systems is a remnant from a time when a server had a handful of cores and processed requests from a few thousand clients. It simply cannot keep up with the scale of modern servers and the requirements of modern applications. Specifically, real-time applications and high user expectations enforce strict performance requirements on the infrastructure. Further, there is a fundamental shift in the way hardware capacity scales from simply relying on Moore's law to deliver faster hardware every couple of years to leveraging parallel processing and task-specific accelerators. This talk covers innovations in three key components of the network stack. First, I will cover my work on scalable packet scheduling in software network stacks, improving the control of traffic outgoing from large-scale servers. Second, I will move on to my work on improving overload control for servers handling microsecond-scale remote procedure calls, providing better control over incoming traffic to large-scale servers. Then, the talk covers my work on Wide Area Network (WAN) congestion control, focusing on network-assisted congestion control schemes, where end-to-end solutions fail. The talk will conclude with a discussion of plans for future research in this area.

--

Please contact MPI-SWS office team for Zoom link information

Several major innovations in artificial intelligence (AI) (e.g. convolutional neural networks, experience replay) are based on findings about the brain. However, the underlying brain findings took many years to first consolidate and many more to transfer to AI. Moreover, these findings were made using invasive methods in non-human species. For cognitive functions that are uniquely human, such as natural language processing, there is no suitable model organism and a mechanistic understanding is that much farther away. In this talk, I will present my research program that circumvents these limitations by establishing a direct connection between the human brain and AI systems with two main goals: 1) to improve the generalization performance of AI systems and 2) to improve our mechanistic understanding of cognitive functions. Lastly, I will discuss future directions that build on these approaches to investigate the role of memory in meaning composition, both in the brain and AI. This investigation will lead to methods that can be applied to a wide range of AI domains, in which it is important to adapt to new data distributions, continually learn to perform new tasks, and learn from few samples.

Please contact MPI-SWS Office Team for link information

This talk reports Facebook's experience of managing the backbone network during the COVID-19 crisis. Our philosophy centers around "risk prevention" to identify potential failures in the network and mitigate their effects. We define metrics for network risk and quantify the impact of COVID-19 with them. We also describe a risk assessment system that has been in production for three years, which involves accurate failure modeling and efficient risk simulation. With ten months of assessment results, we claim our backbone to be robust against the COVID-19 stress test, achieving high service availability and low routing dilation. We share our operational measures to minimize possible traffic loss. Surprising findings during this period give us insights to further improve our approach. First, we observe a substantial reduction of optical failures because of less human activity, which inspires failure prediction to trade model stability for agility by considering short-term failure statistics when necessary. Second, we find a negative correlation between network traffic and human mobility, indicating non- networking signals traditionally ignored can be used for better network management.

LLVM is an industrial-strength compiler that's used for everything from day-to-day iOS development (in Swift) to pie-in-the-sky academic research projects. This makes the LLVM framework a sweet spot for bug-finding and verification technologies--any improvements to it are amplified across its many applications.

This talk asks the question: what does LLVM code _mean_, and, how can we ensure that LLVM-based tools (compilers, optimizers, code instrumentation passes, etc.) do what they're supposed to -- especially for safety- or security-critical applications? The Verified LLVM project (Vellvm) is our attempt to provide an answer. Vellvm gives a semantics to LLVM IR programs in the Coq interactive theorem prover, which can be used for developing machine-checkable formal properties about LLVM IR programs and transformation passes.

Our approach to modeling LLVM IR semantics uses _interaction trees_, a data structure that is suitable for representing impure, possibly nonterminating programs in dependent type theory. Interaction trees support compositional and modular reasoning about program semantics but are also executable, and hence useful for implementation and testing. We'll see how interaction trees are used in Vellvm and, along the way, we'll get a taste of what LLVM code looks like including some of its trickier semantic aspects. We'll also see (at a high level) how modern interactive theorem provers--in this case, Coq--can be used to verify compiler transformations.

No experience with LLVM or formal verification technologies will be assumed.

--

Please contact office for the Zoom details.

The pivotal role of software in our modern world imposes strong requirements on quality, correctness, and reliability of software systems. The ability to understand program code plays a key role for programmers to fulfill these requirements. Despite significant progress, research on program comprehension has had a fundamental limitation: program comprehension is a cognitive process that cannot be directly observed, which leaves considerable room for (mis)interpretation, uncertainty, and confounding factors. Thus, central questions such as "What makes a good programmer?" and "How should we program?" are surprisingly difficult to answer based on the state of the art.

In this talk, I will report on recent attempts to lift research on program comprehension to a new level. The key idea is to leverage methods from cognitive neuroscience to obtain insights into the cognitive processes involved in program comprehension. Opening the "black box" of human cognition will lead to a breakthrough in understanding the why and how of program comprehension and to a completely new perspective and methodology of measuring program comprehension, with direct implications for programming methodology, language design, and education.