Recent events

Analyzing Sample Correlations for Monte Carlo Rendering

Gurprit Singh
MPI-INF - D4
Joint Lecture Series
13 Mar 2019, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Point patterns and stochastic structures lie at the heart of Monte Carlo based numerical integration schemes. Physically based rendering algorithms have largely benefited from these Monte Carlo based schemes that inherently solve very high dimensional light transport integrals. However, due to the underlying stochastic nature of the samples, the resultant images are corrupted with noise (unstructured aliasing or variance). This also results in bad convergence rates that prohibit using these techniques in more interactive environments (e.g. games, virtual reality). With the advent of smart rendering techniques and powerful computing units (CPUs/GPUs), it is now possible to perform physically based rendering at interactive rates. However, much is left to understand regarding the underlying sampling structures and patterns which are the primary cause of error in rendering.  In this talk, we first revisit the most recent state-of-the-art frameworks that are developed to better understand the impact of samples’ structure on the error and its convergence during Monte Carlo integration. Towards the end, we briefly present our deep learning based approach to generate these samples with correlations.

Feedback-Control for Self-Adaptive Predictable Computing

Martina Maggio
Lund University
SWS Colloquium
13 Mar 2019, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Cloud computing gives the illusion of infinite computational capacity and allows for on-demand resource provisioning. As a result, over the last few years, the cloud computing model has experienced widespread industrial adoption and companies like Netflix offloaded their entire infrastructure to the cloud. However, with even the largest datacenter being of a finite size, cloud infrastructures have experienced overload due to overbooking or transient failures. In essence, this is an excellent opportunity for the design of control solutions, that tackle the problem of mitigating overload peaks, using feedback from the infrastructure. These solutions can then exploit control-theoretical principles and take advantage of the knowledge and the analysis capabilities of control tools to provide formal guarantees on the predictability of the infrastructure behavior. This talk introduces recent research advances on feedback control in the cloud computing domain, together with my research agenda for enhancing predictability and formal guarantees for cloud computing.

Automated Resource Management in Large-Scale Networked Systems

Sangeetha Abdu Jyothi
University of Illinois
SWS Colloquium
11 Mar 2019, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Internet applications rely on large-scale networked environments such as the cloud for their backend support. In these multi-tenanted environments, various stakeholders have diverse goals. The objective of the infrastructure provider is to increase revenue by utilizing the resources efficiently. Applications, on the other hand, want to meet their performance requirements at minimal cost. However, estimating the exact amount of resources required to meet the application needs is a difficult task, even for expert users. Easy workarounds employed for tackling this problem, such as resource over-provisioning, negatively impact the goals of the provider, applications, or both. In this talk, I will discuss the design of application-aware self-optimizing systems through automated resource management that helps meet the varied goals of the provider and applications in large-scale networked environments. The key steps in closed-loop resource management include learning of application resource needs, efficient scheduling of resources, and adaptation to variations in real time. I will describe how I apply this high-level approach in two distinct environments using (a) Morpheus in enterprise clusters, and (b) Patronus in cellular provider networks with geo-distributed micro data centers. I will also touch upon my related work in application-specific context at the intersection of network scheduling and deep learning. I will conclude with my vision for self-optimizing systems including fully automated clouds and an elastic geo-distributed platform for thousands of micro data centers.

Predictable Execution of Real-Time Applications on Many-Core Platforms

Matthias Becker
KTH Royal Institute of Technology
SWS Colloquium
08 Mar 2019, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Nowadays, innovation in many industrial areas is software driven, where existing software functions become more complex and new software functions are constantly introduced. The rapid increase in functionality comes along with a steep increase in software complexity. To cope with this transition, current trends shift away from today’s distributed architectures towards integrated architectures. Here, previously distributed functionality is consolidated on fewer, more powerful, computers. Such a trend can for example be observed in the automotive or avionics domain. This can ease the integration process, reduce the hardware complexity, and ultimately save costs. One promising hardware platform for these powerful embedded computers is the many-core processor. A many-core processor hosts a vast number of compute cores, that are partitioned on clusters which are connected by a Network-on-Chip. However, ensuring that real-time requirements are satisfied in the presence of contention in shared resources, such as memories, remains an open issue. In addition, industrial applications are often subject to timing constraints on the data propagation through a chain of semantically related tasks. Such requirements pose challenges to the system designer as they are only able to verify them after the system synthesis (i.e. very late in the design process). In this talk, we present methods that transform timing constraints on the data propagation delay into precedence constraints between individual task instances. An execution framework for the cluster of the many-core is proposed that allows access to cluster external memory while it avoids contention on shared resources by design. Spatial and temporal isolation between different clusters is provided by a partitioning and configuration of the Network-on-Chip that further reduces the worst-case access times to external memory.

Mitigating data leaks in real world systems

Aastha Mehta
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Proposal
07 Mar 2019, 4:30 pm - 5:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Unintended data disclosures are a major concern for many online services, such as healthcare systems, government departments, and web services. Data may leak over explicit output channels of the systems, for instance due to accidental bugs and misconfigurations in the system. Data may also leak over various side channels, for instance, in a cloud environment where a tenant shares the Cloud provider’s infrastructure with other mutually distrusting tenants.

In this thesis, we address the problem of unintended data disclosures in web services due to both types of causes, i.e. explicit leaks and side channel leaks. Specifically, we propose a system to mitigate explicit leaks due to accidental bugs in database-backed services; and a system to mitigate network side channel leaks in the tenants of an infrastructure-as-a-service (IaaS) Cloud.

In this talk, I will first present a high level overview of the design, implementation, and evaluation of Qapla, which is a system to ensure policy compliance in database-backed services.

Then I will present our ongoing work on the design, implementation, and evaluation of Pacer, which is a system to mitigate network side channels in Cloud tenants. Pacer mitigates network side channels using traffic shaping. Pacer provides a generic abstraction of a traffic shaping tunnel, which encapsulates the tenant's network traffic, and shapes it to make it independent of the tenant's secrets. We present a prototype with Pacer's tunnel endpoints integrated in the Cloud hypervisor and the client OS. Our preliminary evaluation shows that Pacer can enforce traffic shaping securely, while incurring modest overheads on bandwidth, client latencies, and server throughput.

Privacy, Transparency and Trust in the User-Centric Internet

Oana Goga
Université Grenoble Alpes
SWS Colloquium
07 Mar 2019, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
The rise of user-centric Internet systems such as Facebook or Twitter brought security and privacy threats that became out of control in recent years. To make such systems more dependable, my research focuses on three key aspects: (1) privacy: ensure users understand and can control the information that is disclosed about them; (2) transparency: ensure users understand how their data is being used and how it affects the services they receive; and (3) trust: ensure users can evaluate the trustworthiness of content consumed from these systems. 

In this talk, I will share my research efforts in understanding and tackling security and privacy threats in social media targeted advertising. Despite a number of recent controversies regarding privacy violations, lack of transparency, or vulnerability to discrimination or propaganda by dishonest actors; users still have little understanding of what data targeted advertising platforms have about them and why they are shown the ads they see. To address such concerns, Facebook recently introduced the "Why am I seeing this?" button that provides users with an explanation of why they were shown a particular ad. I first investigate the level of transparency provided by this mechanism by empirically measuring whether it satisfies a number of key properties and what are the consequences of the current design choices. To provide a better understanding of the Facebook advertising ecosystem, we developed a tool called AdAnalyst that collects the ads users receive and provides aggregate statistics. I will then share our findings from analyzing data from over 600 real-world AdAnalyst users; in particular on who is advertising on Facebook and how these advertisers are targeting users and customizing ads via the platform. 

Towards Literate Artificial Intelligence

Mrinmaya Sachan
Carnegie Mellon University
SWS Colloquium
05 Mar 2019, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Over the past decade, the field of artificial intelligence (AI) has seen striking developments. Yet, today’s AI systems sorely lack the essence of human intelligence i.e.  our ability to (a) understand language and grasp its meaning, (b) assimilate common-sense background knowledge of the world, and (c) draw inferences and perform reasoning. Before we even begin to build AI systems that possess the aforementioned human abilities, we must ask an even more fundamental question: How would we even evaluate an AI system on the aforementioned abilities? In this talk, I will argue that we can evaluate AI systems in the same way as we evaluate our children - by giving them standardized tests. Standardized tests are administered to students to measure the knowledge and skills gained by them. Thus, it is natural to use these tests to measure the intelligence of our AI systems. Then, I will describe Parsing to Programs (P2P), a framework that combines ideas from semantic parsing and probabilistic programming for situated question answering. We used P2P to build systems that can solve pre-university level Euclidean geometry and Newtonian physics examinations. P2P achieves a performance at least as well as the average student on questions from textbooks, geometry questions from previous SAT exams, and mechanics questions from Advanced Placement (AP) exams. I will conclude by describing implications of this research and some ideas for future work.

A Client-centric Approach to Transactional Datastores

Natacha Crooks
University of Texas at Austin
SWS Colloquium
28 Feb 2019, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Modern applications must collect and store massive amounts of data. Cloud storage offers these applications simplicity: the abstraction of a failure-free, perfectly scalable black-box. While appealing, offloading data to the cloud is not without challenges. Cloud storage systems often favour weaker levels of isolation and consistency. These weaker guarantees introduce behaviours that, without care, can break application logic. Offloading data to an untrusted third party like the cloud also raises questions of security and privacy.

This talk summarises my efforts to improve the performance, the semantics and the security of transactional cloud storage systems. It centers around a simple idea: defining consistency guarantees from the perspective of the applications that observe these guarantees, rather than from the perspective of the systems that implement them. I will discuss how this new perspective brings forth several benefits. First, it offers simpler and cleaner definitions of weak isolation and consistency guarantees. Second, it enables more scalable implementations of existing guarantees like causal consistency. Finally, I will discuss its applications to security: our client-centric perspective allows us to add obliviousness guarantees to transactional cloud storage systems.

New Abstractions for High-Performance Datacenter Applications

Malte Schwarzkopf
MIT CSAIL
SWS Colloquium
18 Feb 2019, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Developing high-performance datacenter applications is complex and time-consuming today, as developers must understand and correctly implement subtle interactions between different backend systems. I describe a new approach that redesigns core datacenter systems around new abstractions: the right abstractions substantially reduce complexity while maintaining the same performance. This saves expensive developer time, uses datacenter servers more efficiently, and can enable new, previously impossible systems and applications. I illustrate the impact of such redesigns with Noria, which recasts web application backends-i.e., databases and caches-as a streaming dataflow computation based on a new abstraction of partial state. Noria's partially-stateful dataflow brings classic databases' familiar query flexibility to scalable dataflow systems, simplifying applications and improving the backend's efficiency. For example, Noria increases the request load handled by a single server by 5-70x compared to state-of-the-art backends. Additional new abstractions from my research increase the efficiency of other datacenter systems (e.g., cluster schedulers), or enable new kinds of systems that, for example, may help protect user data against exposure through application bugs.

Scalable positioning of commodity mobile devices using audio signals

Viktor Erdélyi
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Defense
14 Feb 2019, 9:00 am - 10:30 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
This thesis explores the problem of computing a position map for co-located mobile devices. The positioning should happen in a scalable manner without requiring specialized hardware and without requiring specialized infrastructure (except basic Wi-Fi or cellular access). At events like meetings, talks, or conferences, a position map can aid spontaneous communication among users based on their relative position in two ways. First, it enables users to choose message recipients based on their relative position, which also enables the position-based distribution of documents. Second, it enables senders to attach their position to messages, which can facilitate interaction between speaker and audience in a lecture hall and enables the collection of feedback based on users’ location.

In this thesis, we present Sonoloc, a mobile app and system that, by relying on acoustic signals, allows a set of commodity smart devices to determine their relative positions. Sonoloc can position any number of devices within acoustic range with a constant number of acoustic signals emitted by a subset of devices. Our experimental evaluation with up to 115 devices in real rooms shows that – despite substantial background noise – the system can locate devices with an accuracy of tens of centimeters using no more than 15 acoustic signals.

Dynamic Symbolic Execution for Software Analysis

Cristian Cadar
Imperial College London
SWS Distinguished Lecture Series
07 Feb 2019, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Symbolic execution is a program analysis technique that can automatically explore and analyse paths through a program. While symbolic execution was initially introduced in the seventies, it has only received significant attention during the last decade, due to tremendous advances in constraint solving technology and effective blending of symbolic and concrete execution into what is often called dynamic symbolic execution. Dynamic symbolic execution is now a key ingredient in many computer science areas, such as software engineering, computer security, and software systems, to name just a few. In this talk, I will discuss recent advances and ongoing challenges in the area of dynamic symbolic execution, drawing upon our experience developing several symbolic execution tools for many different scenarios, such as high-coverage test input generation, bug and security vulnerability detection, patch testing and bounded verification, among many others.

Machine Teaching

Adish Singla
Max Planck Institute for Software Systems
Joint Lecture Series
06 Feb 2019, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Much of the research in machine learning has focused on designing algorithms for discovering knowledge from data and learning a target model. What if there is a ``teacher" who knows the target already, and wants to steer the ``learner" towards this target as quickly as possible?  For instance, in an educational setting, the teacher (e.g., a tutoring system) has an educational goal that she wants to communicate to a student via a set of demonstrations and lessons; in adversarial attacks known as training-set poisoning, the teacher (e.g., a hacking algorithm) manipulates the behavior of a machine learning system by maliciously modifying the training data. This lecture will provide an overview of machine teaching and cover the following three aspects: (i) how machine teaching differs from machine learning, (ii) highlight the problem space of machine teaching across different dimensions, and (iii) discuss our recent work on developing teaching algorithms for human learners.

Techniques to Protect Confidentiality and Integrity of Persistant and In-Memory Data

Anjo Vahldiek-Oberwagner
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Defense
05 Feb 2019, 5:30 pm - 6:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Today computers store and analyze valuable and sensitive data. As a result we need to protect this data against confidentiality and integrity violations that can result in the illicit release, loss, or modification of a user’s and an organization’s sensitive data such as personal media content or client records. Existing techniques protecting confidentiality and integrity lack either efficiency or are vulnerable to malicious attacks. In this thesis we suggest techniques, Guardat and ERIM, to efficiently and robustly protect persistent and in-memory data. To protect the confidentiality and integrity of persistent data, clients specify per-file policies to Guardat declaratively, concisely and separately from code. Guardat enforces policies by mediating I/O in the storage layer. In contrast to prior techniques, we protect against accidental or malicious circumvention of higher software layers. We present the design and prototype implementation, and demonstrate that Guardat efficiently enforces example policies in a web server. To protect the confidentiality and integrity of in-memory data, ERIM isolates sensitive data using Intel Memory Protection Keys (MPK), a recent x86 extension to partition the address space. However, MPK does not protect against malicious attacks by itself. We prevent malicious attacks by combining MPK with call gates to trusted entry points and ahead-of-time binary inspection. In contrast to existing techniques, ERIM efficiently protects frequently-used session keys of web servers, an in-memory reference monitor’s private state, and managed runtimes from native libraries. These use cases result in high switch rates of the order of 10 5 –10 6 switches/s. Our experiments demonstrate less then 1% runtime overhead per 100,000 switches/s, thus outperforming existing techniques.

Discrimination in Algorithmic Decision Making: From Principles to Measures and Mechanisms

Bilal Zafar
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Defense
04 Feb 2019, 6:00 pm - 7:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
The rise of algorithmic decision making in a variety of applications has also raised concerns about its potential for discrimination against certain social groups. However, incorporating nondiscrimination goals into the design of algorithmic decision making systems (or, classifiers) has proven to be quite challenging. These challenges arise mainly due to the computational complexities involved in the process, and the inadequacy of existing measures to computationally capture discrimination in various situations. The goal of this thesis is to tackle these problems.

First, with the aim of incorporating existing measures of discrimination (namely, disparate treatment and disparate impact) into the design of well-known classifiers, we introduce a mechanism of decision boundary covariance, that can be included in the formulation of any convex boundary-based classifier in the form of convex constraints. Second, we propose alternative measures of discrimination. Our first proposed measure, disparate mistreatment, is useful in situations when unbiased ground truth training data is available. The other two measures, preferred treatment and preferred impact, are useful in situations when feature and class distributions of different social groups are significantly different, and can additionally help reduce the cost of nondiscrimination (as compared to the existing measures). We also design mechanisms to incorporate these new measures into the design of convex boundary-based classifiers.

How to Win a First-Order Safety Game

Helmut Seidl
TUM
SWS Distinguished Lecture Series
01 Feb 2019, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows. Desirable properties of these systems such as functional correctness or non-interference have conveniently been formulated as safety properties. Here, we go one step further. Our goal is to verify safety, and also to develop techniques for automatically synthesizing strategies to enforce safety. For that reason, we generalize FO transition systems to FO safety games. We prove that the existence of a winning strategy of safety player in finite games is equivalent to second-order quantifier elimination. For monadic games, we provide a complete classification into decidable and undecidable cases. For games with non-monadic predicates, we concentrate on universal invariants only. We identify a non-trivial sub-class where safety is decidable. For the general case, we provide meaningful abstraction and refinement techniques for realizing a CEGAR based synthesis loop. Joint work with: Christian Müller, TUM Bernd Finkbeiner, Universität des Saarlandes

Automated Complexity Analysis of Rewrite Systems

Florian Frohn
RWTH Aachen
SWS Colloquium
22 Jan 2019, 10:00 am - 11:00 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Many approaches to analyze the complexity of programs automatically are based on transformations into integer or term rewrite systems. However, state-of-the-art tools that analyze the worst-case complexity of rewrite systems are restricted to the inference of upper bounds. In this talk, the first techniques for the inference of lower bounds on the worst-case complexity of integer and term rewrite systems are introduced. While upper bounds can prove the absence of performance-critical bugs, lower bounds can be used to find them.

For term rewriting, the power of the presented technique gives rise to the question whether the existence of a non-constant lower bound is decidable. Thus, the corresponding decidability results are also discussed in this talk.

Finally, to see the practical value of complexity analysis techniques for rewrite systems, we will have a glimpse at the transformation from Java programs to integer rewrite systems that is implemented in the tool AProVE.

Quantifying & Characterizing Information Diets of Social Media Users

Juhi Kulshrestha
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Defense
20 Dec 2018, 4:00 pm - 5:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
An increasing number of people are relying on online social media platforms like Twitter and Facebook to consume news and information about the world around them. This change has led to a paradigm shift in the way news and information is exchanged in our society – from traditional mass media to online social media.

With the changing environment, it’s essential to study the information consumption of social media users and to audit how automated algorithms (like search and recommendation systems) are modifying the information that social media users consume. In this thesis, we fulfill this high-level goal with a two-fold approach. First, we propose the concept of information diets as the composition of information produced or consumed. Next, we quantify the diversity and bias in the information diets that social media users consume via the three main consumption channels on social media platforms: (a) word of mouth channels that users curate for themselves by creating social links, (b) recommendations that platform providers give to the users, and (c) search systems that users use to find interesting information on these platforms. We measure the information diets of social media users along three different dimensions of topics, geographic sources, and political perspectives.

Our work is aimed at making social media users aware of the potential biases in their consumed diets, and at encouraging the development of novel mechanisms for mitigating the effects of these biases.

Language dynamics in social media

Animesh Mukherjee
Indian Institute of Technology, Kharagpur
SWS Colloquium
13 Dec 2018, 10:30 am - 11:30 am
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 105
In this talk I shall outline a summary of our five year long initiative studying the temporal dynamics of various human language-like entities over the social media. Some of the topics that I plan to cover are (a)  how opinion conflicts could be effectively used for incivility detection in Twitter [CSCW 2018], (b) how word borrowings can be automatically identified from social signals [EMNLP 2017] and (c)  how hashtags in Twitter form compounds like natural language words (e.g., #Wikipedia+#Blackout=#WikipediaBlackout) that become way more popular than the individual constituent hashtags [CSCW 2016, Honorable Mention].

Post-quantum Challenges in Secure Computation

Nico Döttling
CISPA
Joint Lecture Series
05 Dec 2018, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
In the early 1990s cryptography went into a foundational crisis when efficient quantum algorithms were discovered which could break almost all public key encryption schemes known at the time. Since then, a enormous research effort has been invested into basing public key cryptography, and secure computation in general, on problems which are conjectured to be hard even for quantum computers. While this research program has been resoundingly successful, even leading up the way to cryptographic milestones such as fully homomorphic encryption, there are still important cryptographic primitives for which no post-quantum secure protocols are known. Until very recently, one such primitive was 2-message oblivious transfer, a fundamental primitive in the field of secure two- and multi-party computation. I will discuss a novel construction of this primitive from the Learning With Errors (LWE) assumption, a lattice-based problem which is known to be as hard as worst-case lattice problems and conjectured to be post-quantum secure. The security of our construction relies on a fundamental Fourier-analytic property of lattices, namely the transference principle: Either a lattice or its dual must have short vectors.

Privacy-Compliant Mobile Computing

Paarijaat Aditya
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Defense
03 Dec 2018, 4:30 pm - 5:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Sophisticated mobile computing, sensing and recording devices like smartphones, smartwatches, and wearable cameras are carried by their users virtually around the clock, blurring the distinction between the online and offline worlds. While these devices enable transformative new applications and services, they also introduce entirely new threats to users' privacy, because they can capture a complete record of the user's location, online and offline activities, and social encounters, including an audiovisual record. Such a record of users' personal information is highly sensitive and is subject to numerous privacy risks. In this thesis, we have investigated and built systems to mitigate two such privacy risks: 1) privacy risks due to ubiquitous digital capture, where bystanders may inadvertently be captured in photos and videos recorded by other nearby users, 2) privacy risks to users' personal information introduced by a popular class of apps called `mobile social apps'. In this thesis, we present two systems, called I-Pic and EnCore, built to mitigate these two privacy risks.

Both systems aim to put the users back in control of what personal information is being collected and shared, while still enabling innovative new applications. We built working prototypes of both systems and evaluated them through actual user deployments. Overall we demonstrate that it is possible to achieve privacy-compliant digital capture and it is possible to build privacy-compliant mobile social apps, while preserving their intended functionality and ease-of-use. Furthermore, we also explore how the two solutions can be merged into a powerful combination, one which could enable novel workflows for specifying privacy preferences in image capture that do not currently exist.

Survey Equivalence: An Information-theoretic Measure of Classifier Accuracy When the Ground Truth is Subjective

Paul Resnick
University of Michigan, School of Information
SWS Distinguished Lecture Series
27 Nov 2018, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 111
Many classification tasks have no objective ground truth. Examples include: which content or explanation is "better" according to some community? is this comment toxic? what is the political leaning of this news article? The traditional modeling approach assumes each item has an objective true state that is perceived by humans with some random error. It fails to account for the fact that people have greater agreement on some items than others. I will describe an alternative model where the true state is a distribution over labels that raters from a specified population would assign to an item. This leads to information gain (mutual information) as a theoretically justified and computationally tractable measure of a classifier's quality, and an intuitive interpretation of information gain in terms of the sample size for a survey that would yield the same expected error rate.

The Reachability Problem for Vector Addition Systems is Not Elementary

Wojciech Czerwiński
University of Warsaw
SWS Colloquium
22 Nov 2018, 4:00 pm - 5:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
I will present a recent non-elementary lower bound for the complexity of reachability problem for Vector Addition Systems. I plan to show the main insights of the proof. In particular I will present a surprising equation on fractions, which is the core of the new source of hardness found in VASes.

More Realistic Scheduling Models and Analyses for Advanced Real-Time Embedded Systems

Georg von der Brueggen
TU Dortmund
SWS Colloquium
22 Nov 2018, 2:30 pm - 3:30 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
In real-time embedded systems, for each task the compliance to timing constraints has to be guaranteed in addition to the functional correctness. The first part of the talk considers the theoretical comparison of scheduling algorithms and schedulability tests by evaluating speedup factors for non-preemptive scheduling, which leads to a discussion about general problems of resource augmentation bounds. In addition, it is explained how utilization bounds can be parametrized, resulting in better bounds for specific scenarios, i.e., when analyzing non-preemptive Rate-Monotonic scheduling as well as task sets inspired by automotive applications.

In the second part, a setting similar to mixed-criticality systems is considered and the criticism on previous work in this area is detailed. Hence, a new system model that allows a better applicability to realistic scenarios, namely Systems with Dynamic Real-Time Guarantees, is explained. This model is extended to a multiprocessor scenario, considering CPU overheating as a possible cause for mixed-criticality behaviour. Finally, a way to determine the deadline-miss probability for such systems is described that drastically reduces the runtime of such calculations.

The third part discusses tasks with self-suspension behaviour, explains a fixed-relative-deadline strategy for segmented self-suspension tasks with one suspension interval, and details how this approach can be exploited in a resource-oriented partitioned scheduling. Furthermore, it is explained how the gap between the dynamic and the segmented self-suspension model can be bridged by hybrid models.

Verified Secure Routing

Peter Müller
ETH Zurich
SWS Distinguished Lecture Series
19 Nov 2018, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
SCION is a new Internet architecture that addresses many of the security vulnerabilities of today’s Internet. Its clean-slate design provides, among other properties, route control, failure isolation, and multi-path communication. The verifiedSCION project is an effort to formally verify the correctness and security of SCION. It aims to provide strong guarantees for the entire architecture, from the protocol design to its concrete implementation. The project uses stepwise refinement to prove that the protocol withstands increasingly strong attackers. The refinement proofs assume that all network components such as routers satisfy their specifications. This property is then verified separately using deductive program verification in separation logic. This talk will give an overview of the verifiedSCION project and explain, in particular, how we verify code-level properties such as memory safety, I/O behavior, and information flow security.

Feedback Control for Predictable Cloud Computing

Dr. Martina Maggio
Lund University
SWS Colloquium
14 Nov 2018, 10:30 am - 12:00 pm
Saarbrücken building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Cloud computing gives the illusion of infinite computational capacity and allows for on-demand resource provisioning. As a result, over the last few years, the cloud computing model has experienced widespread industrial adoption and companies like Netflix offloaded their entire infrastructure to the cloud. However, with even the largest datacenter being of a finite size, cloud infrastructures have experienced overload due to overbooking or transient failures. In essence, this is an excellent opportunity for the design of control solutions, that tackle the problem of mitigating overload peaks, using feedback from the computing infrastructure. Exploiting control-theoretical principles and taking advantage of the knowledge and the analysis capabilities of control tools, it is possible to provide formal guarantees on the predictability of the cloud platform. This talk introduces recent research advances on feedback control in the cloud computing domain. This talk discusses control solutions and future research for both cloud application development, and infrastructure management. In particular, it covers application brownout, control-based load-balancing, and autoscaling.

Learning from the People: From Normative to Descriptive Solutions to Problems in Security, Privacy & Machine Learning

Elissa Redmiles
University of Maryland
SWS Colloquium
13 Nov 2018, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
A variety of experts -- computer scientists, policy makers, judges -- constantly make decisions about best practices for computational systems. They decide which features are fair to use in a machine learning classifier predicting whether someone will commit a crime, and which security behaviors to recommend and require from end-users. Yet, the best decision is not always clear. Studies have shown that experts often disagree with each other and, perhaps more importantly, with the people for whom they are making these decisions: the users.

This raises a question: Is it possible to learn best practices directly from the users? The field of moral philosophy suggests yes, through the process of descriptive decision-making, in which we observe people’s preferences and then infer best practice rather than using experts’ normative (prescriptive) determinations to define best practice. In this talk, I will explore the benefits and challenges of applying such a descriptive approach to making computationally relevant decisions regarding: (i) selecting security prompts for an online system; (ii) determining which features to include in a classifier for jail sentencing; (iii) defining standards for ethical virtual reality content.

Fairness for Sequential Decision Making Algorithms

Hoda Heidari
ETH Zurich
SWS Colloquium
12 Nov 2018, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
Fairness considerations in settings where decisions are made by supervised learning algorithms (e.g. criminal risk assessment) has received considerable attention, recently. As the fairness literature continues to expand mostly around this canonical learning task, it is important to recognize that many real-world applications of ML fall outside the category of supervised, one-shot learning. In this presentation, I will talk about two scenarios in which algorithmic decisions are made in a sequential manner and over time. I will argue that in such settings, being fair---at a minimum---requires decisions to be "consistent" across individuals who arrive at different time steps, that is, similar individuals must be treated similarly. I will then talk about how such consistency constraints affect learning. 

In the first part of the talk, I will introduce a generic sequential decision making framework, in which at each time step the learning algorithm receives data corresponding to a new individual (e.g. a new job application) and must make an irrevocable decision about him/her (e.g. whether to hire the applicant) based on observations it has made so far. I propose a general framework for post-processing predictions made by a black-box learning model, so that the resulting sequence of outcomes is guaranteed to be consistent. I show, both theoretically and via simulations, that imposing consistency constraints will not significantly slow down learning.

In the second part of the talk, I will focus on fairness considerations in a particular type of market---namely, combinatorial prediction markets---where traders can submit limit orders on various security bundles, and the market maker is tasked with executing these orders in a fair manner. The main challenge in running such market is that executing one order can potentially change the price of every other order in the book. I define the notion of a "fair trading path", which at a high level guarantees similar orders are executed similarly: no order executes at a price above its limit, and every order executes when its market price falls below its limit price. I present a market algorithm that respects these fairness conditions, and evaluate it using real combinatorial predictions made during the 2008 U.S. Presidential election. 

I will conclude by comparing my work with previous papers on fairness for online learning, and a list of directions for future work.

Generating Software Tests

Andreas Zeller
Fachrichtung Informatik - Saarbrücken/CISPA
Joint Lecture Series
07 Nov 2018, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Software has bugs. What can we do to find as many of these as possible? In this talk, I show how to systematically test software by generating such tests automatically, starting with simple random "fuzzing" generators and then proceeding to more effective grammar-based and coverage-guided approaches. Being fully automatic and easy to deploy, such fuzzers run at little cost, yet are very effective in finding bugs: Our own Langfuzz grammar-based test generator for JavaScript runs around the clock for the Firefox, Chrome, and Edge web browsers and so far has found more than 2,600 confirmed bugs. Our latest test generator prototypes are even able to automatically learn the input language of a given program, which allows to generate highly effective tests for arbitrary programs without any particular setup.

Compiling Dynamical Systems for Efficient Simulation on Reconfigurable Analog Computers

Sara Achour
MIT
SWS Colloquium
22 Oct 2018, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Programmable analog devices are a powerful new computing substrate that are especially appropriate for performing computationally intensive simulations of dynamical systems. Until recently, the de-facto standard for programming these devices required hardware specialists to manually program the analog device to model the dynamical system of interest. In this talk, I will present Arco, a compiler that automatically configures analog devices to perform dynamical system simulation, and Jaunt, a compilation technique that that scales dynamical system parameters to change the speed of the simulation and render the resulting simulation physically realizable given the operating constraints of the analog hardware platform. These techniques capture the domain knowledge required to fully exploit the capabilities of reconfigurable analog devices, eliminating a key obstacle to the widespread adoption of these devices.

Justified representation in multiwinner voting: axioms and algorithms

Edith Elkind
University of Oxford
SWS Distinguished Lecture Series
19 Oct 2018, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Suppose that a group of voters wants to select k \ge 1 alternatives from a given set, and each voter indicates which of the alternatives are acceptable to her: the alternatives could be conference submissions, applicants for a scholarship or locations for a fast food chain. In this setting it is natural to require that the winning set represents the voters fairly, in the sense that large groups of voters with similar preferences have at least some of their approved alternatives in the winning set. We describe several ways to formalize this idea, and show how to use it to classify voting rules. For one of our axioms, the only known voting rule that satisfies it is not polynomial-time computable, and it was conjectured that no voting rule that satisfies this axiom can be polynomial-time computable; however, we will show that this is not the case.

AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation

Dana Drachsler Cohen
ETH Zurich
SWS Colloquium
15 Oct 2018, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
In this talk, I will present AI2, a sound and scalable analyzer for deep neural networks. Based on overapproximation, AI2 can automatically prove safety properties (e.g., robustness) of realistic neural networks (e.g., convolutional neural networks). The key insight behind AI2 is to phrase reasoning about safety and robustness of neural networks in terms of classic abstract interpretation, enabling to leverage decades of advances in that area. To this end, I will introduce abstract transformers that capture the behavior of fully connected and convolutional neural network layers with rectified linear unit activations (ReLU), as well as max pooling layers. This allows to handle real-world neural networks, which are often built out of these types of layers. I will also empirically demonstrate that (i) AI2 is precise enough to prove useful specifications (e.g., robustness), (ii) AI2 can be used to certify the effectiveness of state-of-the-art defenses for neural networks, and (iii) AI2 is significantly faster than existing analyzers based on symbolic analysis, which often take hours to verify simple fully connected networks.

Complexity in Question Answering

Rishiraj Saha Roy
MPI-INF - D5
Joint Lecture Series
10 Oct 2018, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Answering natural-language questions is a remarkable ability of search engines. However, brittleness in the state-of-the-art is exposed when handling complexity in question formulation. Such complexity has two distinct dimensions: (i) diversity of expressions which convey the same information need, and, (ii) complexity in the information need itself. We propose initial solutions to these challenges: (i) syntactic differences in question formulation can be tackled with a continuous-learning framework that extends template-based answering with semantic similarity and user feedback; (ii) complexity in information needs can be addressed by stitching pieces of evidence from multiple documents to build a noisy graph, within which answers can be detected using optimal interconnections. The talk will discuss results for these proposals, and conclude with promising open directions in question answering.