Recent events

Towards Usability in Private Data Analytics

Reinhard Munz Max Planck Institute for Software Systems
06 Dec 2019, 2:00 pm - 3:00 pm
Kaiserslautern building G26, room 607
simultaneous videocast to Saarbrücken building E1 5, room 005 / Meeting ID: 6312
SWS Student Defense Talks - Thesis Defense
Private data analytics systems preferably provide required analytic accuracy to analysts and specified privacy to individuals whose data is analyzed. Devising a general system that works for a broad range of datasets and analytic scenarios has proven to be difficult.

Differentially private systems allow for proven formal privacy guarantees. To provide these guarantees, however, differentially private mechanisms often need to add large amounts of noise to statistical results, which impairs their usability. Thus, despite the advent of mechanisms with formal guarantees, …
Private data analytics systems preferably provide required analytic accuracy to analysts and specified privacy to individuals whose data is analyzed. Devising a general system that works for a broad range of datasets and analytic scenarios has proven to be difficult.

Differentially private systems allow for proven formal privacy guarantees. To provide these guarantees, however, differentially private mechanisms often need to add large amounts of noise to statistical results, which impairs their usability. Thus, despite the advent of mechanisms with formal guarantees, industry still uses inferior ad-hoc mechanisms that provide better analytic accuracy.

In my thesis I follow two approaches to improve the usability of private data analytics systems in general and differentially private systems in particular. First, I revisit ad-hoc mechanisms and explore the possibilities of systems that do not provide Differential Privacy or only a weak version thereof. Based on an attack analysis, I devise a set of new protection mechanisms including Query Based Bookkeeping (QBB). In contrast to previous systems, QBB only requires the history of analysts’ queries in order to provide privacy protection, but does NOT require any knowledge about the protected individuals’ data.

In my second approach I use the insights gained with QBB to propose UniTraX, the first differentially private analytics system that allows analysts to analyze part of a protected dataset without affecting the other parts and without giving up on accuracy. I show UniTraX’s usability by way of multiple case studies on real-world datasets across different domains. In all cases I demonstrate that UniTraX allows more queries than previous differentially private data analytics systems at moderate runtime overheads.
Read more

Stronger Higher-order Automation

Sophie Tourret MPI-INF - RG 1
04 Dec 2019, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
Automated reasoning in first-order logic (FOL) is becoming a mature research domain. It has led to the development of powerful tools such as superposition-based theorem provers and SMT solvers (Satisfiability Modulo Theory solvers), that have found and continue to find many applications in industry and research.

One such application is the automation of proofs in interactive theorem proving (ITP), where proof assistants are used to write computer-checked proofs of theorems, generally expressed in a variant of higher-order logic (HOL). …
Automated reasoning in first-order logic (FOL) is becoming a mature research domain. It has led to the development of powerful tools such as superposition-based theorem provers and SMT solvers (Satisfiability Modulo Theory solvers), that have found and continue to find many applications in industry and research.

One such application is the automation of proofs in interactive theorem proving (ITP), where proof assistants are used to write computer-checked proofs of theorems, generally expressed in a variant of higher-order logic (HOL). This automation is realised via "hammers", that attempt to delegate the proof obligations to first-order automated provers. However, in the translation from HOL to FOL, hammers obfuscate the structure of terms and formulas through the application of a sequence of encodings, although it is this very structure that the provers exploit to find proofs efficiently.

This situation is less than ideal, and if until a few years ago, the ITP and ATP communities were working in parallel, mostly ignoring each other, there is nowadays a trend pushing to bring the two communities closer. The work that I will present in this talk is part of this trend. It includes ongoing research that is either improving higher-order automation with respect to ITP applications or using ITP as a vehicle for ATP research.
Read more

Prusti – Deductive Verification for Rust

Alex Summers ETH Zurich
03 Dec 2019, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029 / Meeting ID: 6312
SWS Colloquium
Producing reliable systems software is a major challenge, plagued by the ubiquitous problems of shared mutable state, pointer aliasing, dynamic memory management, and subtle concurrency issues such as race conditions; even expert programmers struggle to tame the wide variety of reasons why their programs may not behave as they intended. Formal verification offers potential solutions to many of these problems, but typically at a very high price: the mathematical techniques employed are highly-complex, and difficult for even expert researchers to understand and apply. …
Producing reliable systems software is a major challenge, plagued by the ubiquitous problems of shared mutable state, pointer aliasing, dynamic memory management, and subtle concurrency issues such as race conditions; even expert programmers struggle to tame the wide variety of reasons why their programs may not behave as they intended. Formal verification offers potential solutions to many of these problems, but typically at a very high price: the mathematical techniques employed are highly-complex, and difficult for even expert researchers to understand and apply.

The relatively-new Rust programming language is designed to help with the former problem: a powerful ownership type system requires programmers to specify and restrict their discipline for referencing heap locations, providing in return the strong guarantee (almost – the talk, and Rustbelt!) that code type-checked by this system will be free from dangling pointers, unexpected aliasing, race conditions and the like. While this rules out a number of common errors, the question of whether a program behaves as intended remains.

In this talk, I’ll give an overview of the Prusti project, which leverages Rust’s type system and compiler analyses for formal verification. By combining the rich information available about a type-checked Rust program with separate user-specification of intended behaviour, Prusti enables a user to verify functional correctness of their code without interacting with a complex program logic; in particular, specifications and all interactions with our implemented tool are at the level of abstraction of Rust expressions.
Read more

Personal Knowledge Extraction: What Can Be Inferred From What You Say and Do

Paramita Mirza MPI-INF - D5
06 Nov 2019, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
Despite recent advances in natural language processing and generation, communication between humans and machines is in still its infancy. Existing intelligent home and mobile assistant technologies excel at scripted tasks such as weather or news reports and music control, yet typically fail at more advanced personalization. This calls for a centralized repository for personal knowledge about each user, which will then be a distant source of background knowledge for personalization in downstream applications. Such personal knowledge repository will be beneficial as a reusable asset; …
Despite recent advances in natural language processing and generation, communication between humans and machines is in still its infancy. Existing intelligent home and mobile assistant technologies excel at scripted tasks such as weather or news reports and music control, yet typically fail at more advanced personalization. This calls for a centralized repository for personal knowledge about each user, which will then be a distant source of background knowledge for personalization in downstream applications. Such personal knowledge repository will be beneficial as a reusable asset; it should be both explainable and scrutable, giving full control to the owning user on editing and sharing stored information with selected service providers.

In this talk, I will discuss our efforts on automated personal knowledge extraction. We can easily obtain personal knowledge of famous people from biographies or news articles, however, such resources are not available for ordinary users. Hence, we turn to the task of inferring personal attributes from users' utterances in conversations, e.g., guessing a person's occupation from "I was sitting the whole day in front of my computer today, trying to finish a grant proposal for my research." I will highlight our Hidden Attribute Models (HAM) to solve the problem, a neural architecture leveraging attention mechanisms and embeddings, as well as an ongoing work on its extension to address challenging attributes such as hobbies and travel preferences with wide sets of multi-faceted attribute values. Finally, I will present an outlook on what we can further infer from users' activities, particularly in relation with their mood and emotion.
Read more

Dealing with Epidemics under Uncertainty

Jessica Hoffmann University of Texas at Austin
04 Nov 2019, 10:30 am - 11:30 am
Saarbrücken building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029 / Meeting ID: 6312
SWS Colloquium
Epidemic processes can model anything that spreads. As such, they are a useful tool for studying not only human diseases, but also network attacks, chains of activation in the brain, the propagation of real or fake news, the spread of viral tweets, and other processes. In this talk, we investigate epidemics spreading on a graph in the presence of various forms of uncertainty. We present in particular a result about controlling the spread of an epidemic when there is uncertainty about who exactly is infected. …
Epidemic processes can model anything that spreads. As such, they are a useful tool for studying not only human diseases, but also network attacks, chains of activation in the brain, the propagation of real or fake news, the spread of viral tweets, and other processes. In this talk, we investigate epidemics spreading on a graph in the presence of various forms of uncertainty. We present in particular a result about controlling the spread of an epidemic when there is uncertainty about who exactly is infected. We show first that neither algorithms nor results are robust to uncertainty. In other words, uncertainty fundamentally changes how we must approach epidemics on graphs. We also present two related results about learning the graph underlying an epidemic process when there is uncertainty about when people were infected or what infected them.
Read more

Knowledge and Information Dissemination: Models and Methods

Utkarsh Upadhyay Max Planck Institute for Software Systems
17 Oct 2019, 4:00 pm - 5:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029 / Meeting ID: 6312
SWS Student Defense Talks - Thesis Proposal
In the past, information and knowledge dissemination was relegated to the 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 has 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 US population visits Yahoo! …
In the past, information and knowledge dissemination was relegated to the 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 has 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 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, which are better suited to understanding and analysing the dissemination, and to develop new methods to optimize them.

At a broad level, we can view the participation of users in the process of dissemination as falling in 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. The first part of the thesis will propose models for the complexity of discussions and the evolution of expertise. The latter part of the thesis will explore the competitive setting where I will propose computational methods for measuring, and increasing, the attention received from followers on social media.
Read more

Non-Reformist Reform for Haskell Modularity

Scott Kilpatrick Max Planck Institute for Software Systems
15 Oct 2019, 3:00 pm - 4:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111 / Meeting ID: 6747
SWS Student Defense Talks - Thesis Defense
Module systems like that of Haskell permit only a weak form of modularity in which module implementations depend directly on other implementations and must be processed in dependency order. Module systems like that of ML, on the other hand, permit a stronger form of modularity in which explicit interfaces express assumptions about dependencies and each module can be typechecked and reasoned about independently.

In this thesis, I present Backpack, a new language for building separately-typecheckable packages on top of a weak module system like Haskell’s. …
Module systems like that of Haskell permit only a weak form of modularity in which module implementations depend directly on other implementations and must be processed in dependency order. Module systems like that of ML, on the other hand, permit a stronger form of modularity in which explicit interfaces express assumptions about dependencies and each module can be typechecked and reasoned about independently.

In this thesis, I present Backpack, a new language for building separately-typecheckable packages on top of a weak module system like Haskell’s. The design of Backpack is the first to bring the rich world of type systems to the practical world of packages via mixin modules. It’s inspired by the MixML module calculus of Rossberg and Dreyer but by choosing practicality over expressivity Backpack both simplifies that semantics and supports a flexible notion of applicative instantiation. Moreover, this design is motivated less by foundational concerns and more by the practical concern of integration into Haskell. The result is a new approach to writing modular software at the scale of packages.

The semantics of Backpack is defined via elaboration into sets of Haskell modules and binary interface files, thus showing how Backpack maintains interoperability with Haskell while retrofitting it with interfaces. In my formalization of Backpack I present a novel type system for Haskell modules and I prove a key soundness theorem to validate Backpack’s semantics.
Read more

Are We Susceptible to Rowhammer? An End-to-End Methodology for Cloud Providers

Stefan Saroiu Mircosoft Research, Redmond
07 Oct 2019, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 113 / Meeting ID: 6312
SWS Colloquium
Cloud providers are nervous about recent research showing how Rowhammer attacks affect many types of DRAM including DDR4 and ECC-equipped DRAM.  Unfortunately, cloud providers lack a systematic way to test the DRAM present in their servers for the threat of a Rowhammer attack. Building such a methodology needs to overcome two difficult challenges: (1) devising a CPU instruction sequence that maximizes the rate of DRAM row activations on a given system, and (2) determining the adjacency of rows internal to DRAM. …
Cloud providers are nervous about recent research showing how Rowhammer attacks affect many types of DRAM including DDR4 and ECC-equipped DRAM.  Unfortunately, cloud providers lack a systematic way to test the DRAM present in their servers for the threat of a Rowhammer attack. Building such a methodology needs to overcome two difficult challenges: (1) devising a CPU instruction sequence that maximizes the rate of DRAM row activations on a given system, and (2) determining the adjacency of rows internal to DRAM. This talk will present an end-to-end methodology that overcomes these challenges to determine if cloud servers are susceptible to Rowhammer attacks. With our methodology, a cloud provider can construct worst-case testing conditions for DRAM.

We used our methodology to create worst-case DRAM testing conditions on the hardware used by a major cloud provider for a recent generation of its servers. Our findings show that none of the instruction sequences used in prior work to mount Rowhammer attacks create worst-case DRAM testing conditions. Instead, we construct an instruction sequence that issues non-explicit load and store instructions. Our new sequence leverages microarchitectural side-effects to ``hammer'' DRAM at a near-optimal rate on modern Skylake platforms. We also designed a DDR4 fault injector capable of reverse engineering row adjacency inside a DRAM device. When applied to our cloud provider's DIMMs, we find that rows inside DDR4 DRAM devices do not always follow a linear map.

Joint work with Lucian Cojocar (VU Amsterdam), Jeremie Kim, Minesh Patel, Onur Mutlu (ETH Zurich), Lily Tsai (MIT), and Alec Wolman (MSR)
Read more

Efficient Optimization for Very Large Combinatorial Problems in Computer Vision and Machine Learning

Paul Swoboda MPI-INF - D2
02 Oct 2019, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
In computer vision and machine learning combinatorial optimization problems are widespread, typically NP-hard and tend to pose unique challenges due to their very large scale and problem structure. Established techniques from the mathematical optimization community cannot cope with the encountered problem sizes and do not exploit special problem characteristics. In this talk I will present several new solution paradigms for solving large scale combinatorial problems in computer vision efficiently and to high accuracy. I will discuss how these principles can be applied on classical problems of combinatorial optimization that have found wide use in computer vision, …
In computer vision and machine learning combinatorial optimization problems are widespread, typically NP-hard and tend to pose unique challenges due to their very large scale and problem structure. Established techniques from the mathematical optimization community cannot cope with the encountered problem sizes and do not exploit special problem characteristics. In this talk I will present several new solution paradigms for solving large scale combinatorial problems in computer vision efficiently and to high accuracy. I will discuss how these principles can be applied on classical problems of combinatorial optimization that have found wide use in computer vision, machine learning and computer graphics, namely inference in Markov Random Fields, the quadratic assignment problem and graph decomposition. Lastly, I will show empirical results showing the great practical performance of the presented techniques.
Read more

Toward Cognitive Security

Claude Castelluccia InRIA
02 Oct 2019, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111 / Meeting ID: 6312
SWS Colloquium
Online services, devices or secret services are constantly collecting data and meta-data from users. This data collection is mostly  used to target users or customise their services. However, as illustrated by the Cambridge Analytica case, data and technologies are more and  more used to manipulate, influence or shape people's opinions online, i.e. to "hack" our brains. In this context, it is urgent to develop the field of  "Cognitive security" in order to better comprehend these attacks and provide counter-measures.  …
Online services, devices or secret services are constantly collecting data and meta-data from users. This data collection is mostly  used to target users or customise their services. However, as illustrated by the Cambridge Analytica case, data and technologies are more and  more used to manipulate, influence or shape people's opinions online, i.e. to "hack" our brains. In this context, it is urgent to develop the field of  "Cognitive security" in order to better comprehend these attacks and provide counter-measures.  This talk will introduce the concept of "Cognitive security". We will explore the different types of cognitive attacks and discuss possible research directions.
Read more

Human-Centered Design and Data Science for Good

Maria Rauschenberger Universitat Pompeu Fabra
30 Sep 2019, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112 / Meeting ID: 9312
SWS Colloquium
How can we make better applications for social impact issues? For example, the combination of Human-Centered Design (HCD) and Data Science (DS) can be the answer to avoid biases in the collection of data with online-experiments and the analysis of small data. This presentation shows how we combine HCD and DS to design applications and analyze the collected data for Good.  We will focus mainly on the project: "Early screening of dyslexia using a language-independent content game and machine learning". …
How can we make better applications for social impact issues? For example, the combination of Human-Centered Design (HCD) and Data Science (DS) can be the answer to avoid biases in the collection of data with online-experiments and the analysis of small data. This presentation shows how we combine HCD and DS to design applications and analyze the collected data for Good.  We will focus mainly on the project: "Early screening of dyslexia using a language-independent content game and machine learning". With our two designed games (MusVis and DGames), we collected data sets (313 and 137 participants) in different languages (mainly Spanish and German) and evaluated them with machine learning classifiers. For MusVis, we mainly use content that refers to one single acoustic or visual indicator, while DGames content refers to generic content related to various indicators. Our results open the possibility of low-cost and early screening of dyslexia through the Web. In this talk, we will further address the techniques used from HCD and DS to reach these results. 
Read more

Accelerating Network Applications with Stateful TCP Offloading

YoungGyoun Moon KAIST
24 Sep 2019, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111 / Meeting ID: 6312
SWS Colloquium
The performance of modern key-value servers or layer-7 load balancers often heavily depends on the efficiency of the underlying TCP stack. Despite numerous optimizations such as kernel-bypassing and zero-copying, performance improvement for TCP applications is fundamentally limited due to the protocol conformance overhead for compatible TCP operations.

In this talk, I will introduce AccelTCP, a hardware-assisted TCP stack architecture that harnesses programmable network interface cards (NICs) as a TCP protocol accelerator. AccelTCP can offload complex TCP operations such as connection setup and teardown completely to NIC, …
The performance of modern key-value servers or layer-7 load balancers often heavily depends on the efficiency of the underlying TCP stack. Despite numerous optimizations such as kernel-bypassing and zero-copying, performance improvement for TCP applications is fundamentally limited due to the protocol conformance overhead for compatible TCP operations.

In this talk, I will introduce AccelTCP, a hardware-assisted TCP stack architecture that harnesses programmable network interface cards (NICs) as a TCP protocol accelerator. AccelTCP can offload complex TCP operations such as connection setup and teardown completely to NIC, which frees a significant amount of host CPU cycles for application processing. In addition, for layer-7 proxies, it supports running connection splicing on NIC so that the NIC relays all packets of the spliced connections with zero DMA overhead. We showcase the effectiveness of AccelTCP with two real-world applications: (1) Redis, a popular in-memory key-value store, and (2) HAProxy, a widely-used layer-7 load balancer. Our evaluation shows that AccelTCP improves their performance by 2.3x and 11.9x, respectively.
Read more

Synthesis from within: implementing automated synthesis inside an SMT solver

Cesare Tinelli University of Iowa
16 Sep 2019, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Kaiserslautern building E1 5, room 029 / Meeting ID: 6312
SWS Colloquium
Recent research in automated software synthesis from specifications or observations has leveraged the power of SMT solvers in order to explore the space of synthesis conjectures efficiently. In most of this work, synthesis techniques are built around a backend SMT solver which is used as a black-box reasoning engine. In this talk, I will describe a successful multiyear research effort by the developers of the SMT solver CVC4 that instead incorporates synthesis capabilities directly within the solver, …
Recent research in automated software synthesis from specifications or observations has leveraged the power of SMT solvers in order to explore the space of synthesis conjectures efficiently. In most of this work, synthesis techniques are built around a backend SMT solver which is used as a black-box reasoning engine. In this talk, I will describe a successful multiyear research effort by the developers of the SMT solver CVC4 that instead incorporates synthesis capabilities directly within the solver, and the discuss the advances in performance and scope made possible by this approach.
Read more

Computational Fabrication: 3D Printing and Beyond

Vahid Babaei MPI-INF - D4
04 Sep 2019, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
The objective of my talk is to introduce the audience to the exciting field of computational fabrication. The recent, wide availability of 3D printers has triggered considerable interest in academia and industry. Computer scientists could engage with hands-on 3D printing and very soon realize the immense but untapped potential of the manufacturing industry for computational methods. In this talk, I will explain the principles of 3D printing (also known as additive manufacturing) both from hardware and software viewpoints. …
The objective of my talk is to introduce the audience to the exciting field of computational fabrication. The recent, wide availability of 3D printers has triggered considerable interest in academia and industry. Computer scientists could engage with hands-on 3D printing and very soon realize the immense but untapped potential of the manufacturing industry for computational methods. In this talk, I will explain the principles of 3D printing (also known as additive manufacturing) both from hardware and software viewpoints. I will then show examples of recent research addressing computational problems in both 3D printing and general manufacturing. I will also discuss my main research interest, i.e. computational fabrication of visual appearance. Appearance of objects is among their most important and most complicated properties that influence or in numerous cases define their function. I show that additive manufacturing provides unprecedented opportunities to create products with novel and useful appearance properties.
Read more

A type theory for amortized resource analysis

Vineet Rajani Max Planck Institute for Software Systems
27 Aug 2019, 2:00 pm - 3:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111 / Meeting ID: 6312
SWS Student Defense Talks - Thesis Proposal
Amortized analysis is a standard algorithmic technique for estimating upper bounds on the average costs of functions, specifically operations on data structures. This thesis intends to develop λ-amor, a type-theory for amortized analysis of higher-order functional programs. A typical amortized analysis works by storing ghost resource called /potential/ with a data structure's internal state. Accordingly, the central idea in λ-amor is a type-theoretic construct to associate potential with an arbitrary type. Additionally, λ-amor relies on standard concepts from substructural and modal type systems: indexed monads, …
Amortized analysis is a standard algorithmic technique for estimating upper bounds on the average costs of functions, specifically operations on data structures. This thesis intends to develop λ-amor, a type-theory for amortized analysis of higher-order functional programs. A typical amortized analysis works by storing ghost resource called /potential/ with a data structure's internal state. Accordingly, the central idea in λ-amor is a type-theoretic construct to associate potential with an arbitrary type. Additionally, λ-amor relies on standard concepts from substructural and modal type systems: indexed monads, affine types and indexed exponential types. We show that λ-amor is not only sound (in a very elementary logical relations model), but also very expressive: It can be used to analyze both eager and lazy data structures, and it can embed existing resource analysis frameworks. In fact, λ-amor is /complete/ for the cost analysis of lazy PCF programs. Further, the basic principles behind λ-amor can be adapted (by dropping affineness and adding mutable state) to obtain an expressive type system for a completely unrelated application, namely, information flow control.

The proposal talk will cover the broad setting and the motivation of the work and a significant subset of λ-amor, but due to time constraints, it will not cover all of λ-amor or the adaptation to information flow control. Implementation of the two type theories is not in the scope of the thesis.
Read more

Modeling and Individualizing Learning in Computer-Based Environments

Tanja Käser Stanford University
21 Aug 2019, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112 / Meeting ID: 6312
SWS Colloquium
Learning technologies are becoming increasingly important in today's education. This includes game-based learning and simulations, which produce high volume output, and MOOCs (massive open online courses), which reach a broad and diverse audience at scale. The users of such systems often are of very different backgrounds, for example in terms of age, prior knowledge, and learning speed. Adaptation to the specific needs of the individual user is therefore essential. In this talk, I will present two of my contributions on modeling and predicting student learning in computer-based environments with the goal to enable individualization. …
Learning technologies are becoming increasingly important in today's education. This includes game-based learning and simulations, which produce high volume output, and MOOCs (massive open online courses), which reach a broad and diverse audience at scale. The users of such systems often are of very different backgrounds, for example in terms of age, prior knowledge, and learning speed. Adaptation to the specific needs of the individual user is therefore essential. In this talk, I will present two of my contributions on modeling and predicting student learning in computer-based environments with the goal to enable individualization. The first contribution introduces a new model and algorithm for representing and predicting student knowledge. The new approach is efficient and has been demonstrated to outperform previous work regarding prediction accuracy. The second contribution introduces models, which are able to not only take into account the accuracy of the user, but also the inquiry strategies of the user, improving prediction of future learning. Furthermore, students can be clustered into groups with different strategies and targeted interventions can be designed based on these strategies. Finally, I will also describe lines of future research.
Read more

Computer Science for Numerics

Martin Ziegler KAIST
19 Jul 2019, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111 / Meeting ID: 6312
SWS Colloquium
Since introduction of the IEEE 754 floating point standard in 1985, numerical methods have become ubiquitous --- and increasingly sophisticated. With growing code complexity of numerical libraries grows the need for rigorous Software Engineering methodology: as provided by Computer Science and state of the art regarding digital processing of discrete data, but lacking in the continuous realm. We apply, adapt, and extend the classical concepts --- specification, algorithmics, analysis, complexity, verification --- from discrete bit strings, …
Since introduction of the IEEE 754 floating point standard in 1985, numerical methods have become ubiquitous --- and increasingly sophisticated. With growing code complexity of numerical libraries grows the need for rigorous Software Engineering methodology: as provided by Computer Science and state of the art regarding digital processing of discrete data, but lacking in the continuous realm. We apply, adapt, and extend the classical concepts --- specification, algorithmics, analysis, complexity, verification --- from discrete bit strings, integers, graphs etc. to real numbers, converging sequences, smooth/integrable functions, bounded operators, and compact subsets: A new paradigm formalizes mathematical structures as continuous Abstract Data Types with rigorous Turing-computable semantics but without the hassle of actual Turing machines.
Read more

Correct Compilation of Relaxed Memory Concurrency

Soham Chakraborty Max Planck Institute for Software Systems
16 Jul 2019, 1:00 pm - 2:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 005 / Meeting ID: 6312
SWS Student Defense Talks - Thesis Defense
Shared memory concurrency is the pervasive programming model for multicore architectures such as X86, Power, and ARM. Depending on the memory organization, each architecture follows a somewhat different shared memory model. All these models, however, have one common feature: they allow certain outcomes for concurrent programs that cannot be explained by interleaving execution. In addition to the complexity due to architectures, compilers like GCC and LLVM perform various program transformations, which also affect the outcomes of concurrent programs. …
Shared memory concurrency is the pervasive programming model for multicore architectures such as X86, Power, and ARM. Depending on the memory organization, each architecture follows a somewhat different shared memory model. All these models, however, have one common feature: they allow certain outcomes for concurrent programs that cannot be explained by interleaving execution. In addition to the complexity due to architectures, compilers like GCC and LLVM perform various program transformations, which also affect the outcomes of concurrent programs.

To be able to program these systems correctly and effectively, it is important to a define a formal language-level concurrency model. For efficiency, it is important that the model is weak enough to allow various compiler optimizations on shared memory accesses as well as efficient mappings to the architectures. For programmability, the model should be strong enough to disallow bogus "out- of-thin-air" executions and provide strong guarantees for well synchronized programs. Because of these conflicting requirements, defining such a formal model is very difficult. This is why, despite years of research, major programming languages such as C/C++ and Java do not yet have completely adequate formal models defining their concurrency semantics.

In this thesis, we address this challenge and develop a formal concurrency model that is very good both in terms of compilation efficiency and of programmability. Unlike most previous approaches, which were defined either operationally or axiomatically on single executions, our formal model is based on event structures, which represents multiple program executions, and thus gives us more structure to define the semantics of concurrency.

In more detail, our formalization has two variants: the weaker version, WEAKEST, and the stronger version, WEAKESTMO. The WEAKEST model simulates the promising semantics proposed by Kang et al., while WEAKESTMO is incomparable to the promising semantics. Moreover, WEAKESTMO discards certain questionable behaviors allowed by the promising semantics. We show that the proposed WEAKESTMO model resolve out-of-thin-air problem, provide standard data-race-freedom (DRF) guarantees, allow the desirable optimizations, and can be mapped to the architectures like X86, PowerPC, ARMv7. Additionally, our models are flexible enough to leverage existing results from the literature. In addition, in order to ensure the correctness of compilation by a major compiler, we developed a translation validator targeting LLVM’s "opt" transformations of concurrent C/C++ programs. Using the validator, we identified a few subtle compilation bugs, which were reported and were fixed. Additionally, we observe that LLVM concurrency semantics differs from that of C11; there are transformations which are justified in C11 but not in LLVM and vice versa. Considering the subtle aspects of LLVM concurrency, we formalized a fragment of LLVM’s concurrency semantics and integrated it into our WEAKESTMO model.
Read more

Design Problems: Trustworthy Smart Devices and 3D Printed Lace

Mary Baker HP Labs in Palo Alto
15 Jul 2019, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111 / Meeting ID: 6312
SWS Distinguished Lecture Series
A growing number of domestic spaces incorporate products that collect data from cameras, microphones and other sensors, leading to privacy concerns. In this talk I report on two user studies performed to learn about perceptions of privacy and trust for sensor-enabled, connected devices such as smart home assistants. The study results suggest that users are more likely to trust devices with materially representative privacy status indicators. This means that the indicators themselves are part of what determines what sensing can take place. …
A growing number of domestic spaces incorporate products that collect data from cameras, microphones and other sensors, leading to privacy concerns. In this talk I report on two user studies performed to learn about perceptions of privacy and trust for sensor-enabled, connected devices such as smart home assistants. The study results suggest that users are more likely to trust devices with materially representative privacy status indicators. This means that the indicators themselves are part of what determines what sensing can take place. I will describe how we have applied the study results to the design of current devices and what the implications are for the physical design of future smart devices.

Time permitting, I will also talk about my other current passion -- design for additive manufacturing – and what researchers can do to ensure we reach the vastly exciting potential of this method of production. I will bring exotic 3D printed parts to help demonstrate my points.
Read more

Automated Program Repair

Abhik Roychoudhury National University of Singapore
08 Jul 2019, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029 / Meeting ID: 6312
SWS Distinguished Lecture Series
Automated program repair is an emerging and exciting field of research, which allows for automated rectification of errors and vulnerabilities. The use of automated program repair can be myriad, such as (a) improving programmer productivity (b) automated fixing of security vulnerabilities as they are detected, (c) self-healing software for autonomous devices such as drones, as well as (d) use of repair in introductory programming education by grading and providing hints for programming assignments. One of the key technical challenges in achieving automated program repair, …
Automated program repair is an emerging and exciting field of research, which allows for automated rectification of errors and vulnerabilities. The use of automated program repair can be myriad, such as (a) improving programmer productivity (b) automated fixing of security vulnerabilities as they are detected, (c) self-healing software for autonomous devices such as drones, as well as (d) use of repair in introductory programming education by grading and providing hints for programming assignments. One of the key technical challenges in achieving automated program repair, is the lack of formal specifications of intended program behavior. In this talk, we will conceptualize the use of symbolic execution approaches and tools for extracting such specifications. This is done by analyzing a buggy program against selected tests, or against reference implementations. Such specification inference capability can be combined with program synthesis techniques to automatically repair programs. The capability of specification inference also serves a novel use of symbolic execution beyond verification and navigation of large search spaces. Automated program repair via symbolic execution goes beyond search-based approaches which attempt to lift patches from elsewhere in the program. Such an approach can construct "imaginative" patches, serves as a test-bed for the grand- challenge of automated programming, and contributes to the vision of trustworthy self-healing software. Towards the end of the talk, we can put the research on automated repair in light of the overall practice of software security, by sharing some experiences gained at the Singapore Cyber-security Consortium.
Read more

The Bright and Dark Sides of Computer Vision: Challenges and Opportunities for Privacy and Security

Mario Fritz CISPA
03 Jul 2019, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
Today, vast amounts of visual information is collected and often also shared online. Such images and videos can contain various types of privacy-sensitive information that can nowadays be extracted automatically at a large scale, posing a steadily growing threat to users' privacy. I'll give an overview of our efforts towards understanding and controlling privacy in visual information as well as working towards our overall vision of a Visual Privacy Advisor. More generally speaking, we have seen a quick adoption of machine learning technology in a broad range of application scenarios. …
Today, vast amounts of visual information is collected and often also shared online. Such images and videos can contain various types of privacy-sensitive information that can nowadays be extracted automatically at a large scale, posing a steadily growing threat to users' privacy. I'll give an overview of our efforts towards understanding and controlling privacy in visual information as well as working towards our overall vision of a Visual Privacy Advisor. More generally speaking, we have seen a quick adoption of machine learning technology in a broad range of application scenarios. With such broad deployment, these approaches become part of the attack surface of modern IT infrastructures and therefore new privacy and security risks emerge. Hence, we research attack vectors and defenses of such intelligent systems built on AI and machine learning technology. In particular, I will talk about our latest work on membership inference and model stealing.
Read more

Fake News During the 2016 U.S. Presidential Elections: Prevalence, Agenda, and Stickiness.

Ceren Budak University of Michigan
10 Jun 2019, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 005
simultaneous videocast to Kaiserslautern building G26, room 111 / Meeting ID: 6312
SWS Colloquium
The spread of fake news was one of the most discussed characteristics of the 2016 U.S. Presidential Election. The concerns regarding fake news have garnered significant attention in both media and policy circles, with some journalists even going as far as claiming that results of the 2016 election were a consequence of the spread of fake news. Yet, little is known about the prevalence and focus of such content, how its prevalence changed over time, and how this prevalence related to important election dynamics. …
The spread of fake news was one of the most discussed characteristics of the 2016 U.S. Presidential Election. The concerns regarding fake news have garnered significant attention in both media and policy circles, with some journalists even going as far as claiming that results of the 2016 election were a consequence of the spread of fake news. Yet, little is known about the prevalence and focus of such content, how its prevalence changed over time, and how this prevalence related to important election dynamics. In this talk, I will address these questions by examining social media, news media, and interview data. These datasets allow examining the interplay between news media production and consumption, social media behavior, and the information the electorate retained about the presidential candidates leading up to the election.
Read more