Upcoming events

Type-Driven Program Synthesis

Nadia Polikarpova
MIT CSAIL, Cambridge USA
SWS Colloquium
15 Feb 2017, 10:00 am - 11:00 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Modern programming languages safeguard developers from many typical errors yet more subtle errors-such as violations of security policies-still plague software. Program synthesis has the potential to eliminate such errors by generating executable code from concise and intuitive high-level specifications. Traditionally program synthesis failed to scale to specifications that encode complex behavioral properties of software: these properties are notoriously hard to check even for a given program and so it?s not surprising that finding the right program within a large space of candidates has been considered very challenging. My work tackles this challenge through the design of synthesis-friendly program verification mechanisms which are able to check a large set of candidate programs against a complex specification at once whereby efficiently pruning the search space.

Based on this principle I developed Synquid a program synthesizer that accepts specifications in the form of expressive types and uses a specialized type checker as its underlying verification mechanism. Synquid is the first synthesizer powerful enough to automatically discover provably correct implementations of complex data structure manipulations such as insertion into Red-Black Trees and AVL Trees and normal-form transformations on propositional formulas. Each of these programs is synthesized in under a minute. Going beyond textbook algorithms I created a language called Lifty which uses type-driven synthesis to automatically rewrite programs that violate information flow policies. In our case study Lifty was able to enforce all required policies in a prototype conference management system.

Adventures in Systems Reliability: Replication and Replay

Ali Mashtizadeh
Stanford University
SWS Colloquium
17 Feb 2017, 10:30 am - 1:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
The past decade has seen a rapid acceleration in the development of new and transformative applications in many areas including transportation medicine ?nance and communication. Most of these applications are made possible by the increasing diversity and scale of hardware and software systems. While this brings unprecedented opportunity it also increases the probability of failures and the dif?culty of diagnosing them. Increased scale and transience has also made management increasingly challenging. Devices can come and go for a variety of reasons including mobility failure and recovery and scaling capacity to meet demand. In this talk I will be presenting several systems that I built to address the resulting challenges to reliability management and security. Ori is a reliable distributed ?le system for devices at the network edge. Ori automates many of the tasks of storage reliability and recovery through replication taking advantage of fast LANs and low cost local storage in edge networks. Castor is record/replay system for multi-core applications with predictable and consistently low overheads. This makes it practical to leave record/replay on in production systems to reproduce difficult bugs when they occur and to support recovering from hardware failures through fault tolerance. Cryptographic CFI (CCFI) is a dynamic approach to control flow integrity. Unlike previous CFI systems that rely purely on static analysis CCFI can classify pointers based on dynamic and runtime characteristics. This limits the attacks to only actively used code paths resulting in a substantially smaller attack surface.

Safe, Real-Time Software Reference Architectures for Cyber-Physical Systems

Renato Mancuso
University of Illinois at Urbana- Champaign
SWS Colloquium
21 Feb 2017, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Renato Mancuso is a doctoral candidate in the Department of Computer Science at the University of Illinois at Urbana-Champaign. He is interested in high-performance cyber-physical systems with a specific focus on techniques to enforce strong performance isolation and temporal predictability in multi-core systems. He has published around 20 papers in major conferences and journals. His papers were awarded a best student paper award and a best presentation award at the Real-Time and Embedded Technology and Applications Symposium (RTAS) in 2013 and 2016 respectively. He was the recipient of a Computer Science Excellence Fellowship and a finalist for the Qualcomm Innovation Fellowship. Some of the design principles for real-time multi-core computing proposed in his research have been officially incorporated in recent certification guidelines for avionics systems. They have also been endorsed by government agencies industries and research institutions worldwide. He received a B.S. in Computer Engineering with honors (2009) and a M.S. in Computer Engineering with honors (2012) from the University of Rome "Tor Vergata".

Variational Bayes In Private Settings

Mijung Park
Amsterdam Machine Learning Lab
SWS Colloquium
03 Mar 2017, 10:00 am - 11:00 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Bayesian methods are frequently used for analysing privacy-sensitive datasets including medical records emails and educational data and there is a growing need for practical Bayesian inference algorithms that protect the privacy of individuals' data. To this end we provide a general framework for privacy-preserving variational Bayes (VB) for a large class of probabilistic models called the conjugate exponential (CE) family. Our primary observation is that when models are in the CE family we can privatise the variational posterior distributions simply by perturbing the expected sufficient statistics of the complete-data likelihood. For widely used non-CE models with binomial likelihoods (e.g. logistic regression) we exploit the Polya-Gamma data augmentation scheme to bring such models into the CE family such that inferences in the modified model resemble the original (private) variational Bayes algorithm as closely as possible. The iterative nature of variational Bayes presents a further challenge for privacy preservation as each iteration increases the amount of noise needed. We overcome this challenge by combining: (1) a relaxed notion of differential privacy called concentrated differential privacy which provides a tight bound on the privacy cost of multiple VB iterations and thus significantly decreases the amount of additive noise; and (2) the privacy amplification effect of subsampling mini-batches from large-scale data in stochastic learning. We empirically demonstrate the effectiveness of our method in CE and non-CE models including latent Dirichlet allocation (LDA) Bayesian logistic regression and Sigmoid Belief Networks (SBNs) evaluated on real-world datasets. >

Randomized Algorithms Meets Formal Verification

Justin Hsu
University of Pennsylvania
SWS Colloquium
08 Mar 2017, 10:00 am - 12:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Algorithms and formal verification are two classical areas of computer science. The two fields apply rigorous mathematical proof to seemingly disparate ends---on the one hand analyzing computational efficiency of algorithms; on the other designing techniques to mechanically show that programs are correct.

In this talk I will present a surprising confluence of ideas from these two areas. First I will show how coupling proofs used to analyze random walks and Markov chains correspond to proofs in the program logic pRHL (probabilistic Relational Hoare Logic). This connection enables formal verification of novel probabilistic properties and provides an structured understanding of proofs by coupling. Then I will show how an approximate version of pRHL called apRHL points to a new approximate version of couplings closely related to differential privacy. The corresponding proof technique---proof by approximate coupling---enables cleaner proofs of differential privacy both for humans and for formal verification. Finally I will share some directions towards a possible "Theory AB" blending ideas from both worlds.