## TCS Seminar SeriesPlease tell Hamed Nemati if you want to give a seminar in the series. They are ideally held Mondays after lunch, but exceptions are possible. See also information about informal PhD student seminars. ## TCS Seminar Series Spring 2017-
22 May 2017 at 10:00 in room 1537
**Part I: Future-Proof Software and Part II: How to test the universe? - Efficient Testing of Software Product Lines** (Ina Schaefer, Technische Universität Braunschweig, Germany)Part I: Modern software systems are extremely long-lived and evolve over time in order to adapt to changing user requirements, application contexts or technological changes. This leads to challenges for software design, implementation, quality assurance and re-engineering in order to make those software systems future-proof. In this talk, I will present an overview of ongoing research in my group at the Institute of Software Engineering and Automotive Informatics at TU Braunschweig addressing the challenges of long-living and evolving software systems. I will focus on two areas of our work: (1) applying machine learning techniques for efficient system-level regression testing and (2) similarity-based variability model mining in order to transform grown software systems into well-structured software product line. Part II: Software product line engineering has gained considerable momentum in recent years, both in industry and in academia. A software product line is a family of software products that share a common set of features. Software product lines challenge traditional analysis, test and verification techniques in their quest of ensuring correctness and reliability of software. Simply creating and testing all products of a product line is usually not feasible, due to the potentially exponential number of valid feature combinations. In this talk, I present different strategies for software product line testing and focus on our recent work on incremental test case selection and test case prioritization of efficient product line testing. -
15 May 2017 at 13:15 in room 4523, Lindstedtsvägen 5
**Representations of Monotone Boolean Functions by Linear Programs** (Mateus de Oliveira Oliveira)We introduce the notion of monotone linear-programming circuits (MLP circuits), a model of computation for partial Boolean functions. Using this model, we prove the following results. 1. MLP circuits are superpolynomially stronger than monotone Boolean circuits. 2. MLP circuits are exponentially stronger than monotone span programs. 3. MLP circuits can be used to provide monotone feasibility interpolation theorems for Lovász-Schrijver proof systems, and for mixed Lovász-Schrijver proof systems. 4. The Lovász-Schrijver proof system cannot be polynomially simulated by the cutting-planes proof system. This is the first result showing a separation between these two proof systems. Finally, we discuss connections between the problem of proving lower bounds on the size of MLPs and the problem of proving lower bounds on extended formulations of polytopes. -
08 May 2017 at 12:00 in room 4523, Lindstedtsvägen 5
**Information-theoretic thresholds** (Amin Coja-Oghlan, Goethe University)Vindicating a sophisticated but non-rigorous physics approach called the cavity method, we prove a formula for the mutual information in statistical inference problems induced by random graphs. This general result implies the conjecture on the information-theoretic threshold in the disassortative stochastic block model [Decelle et al.: Phys. Rev. E (2011)] and allows us to pinpoint the exact condensation phase transition in random constraint satisfaction problems such as random graph coloring, thereby proving a conjecture from [Krzakala et al.: PNAS (2007)]. As a further application we establish the formula for the mutual information in Low-Density Generator Matrix codes as conjectured in [Montanari: IEEE Transactions on Information Theory (2005)]. Joint work with Florent Krzakala, Will Perkins and Lenka Zdeborova. -
24 Apr 2017 at 12:00 in room 4523,, Lindstedtsvägen 5
**Dynamic (Minimum) Spanning Forest with Worst-case Update Time** (Thatchaphol Saranurak, TCS group - KTH)We will discuss recent algorithms for dynamically maintaining a (minimum) spanning forest of a graph undergoing edge insertions and deletions. This problem played a central role in the study of dynamic graph algorithms. We provide the "first polynomial improvement" over the long-standing O(sqrt{n}) bound of [Frederickson STOC’83, Eppstein et. al FOCS’92] for dynamic spanning forest problem. Independently, Wulff-Nilsen shows the first polynomial improvement for dynamic minimum spanning forest problems. Both works will be presented in STOC'17. The new crucial techniques are about expanders: 1) an algorithm for decomposing a graph into a collection of expanders in near-linear time, and 2) an algorithm for "repairing" the expansion property of an expander after deleting some edges of it. These techniques can be of independent interest. -
21 Apr 2017 at 12:00 in room 4523
**Witnessing: From Optimization to Verification to Optimization** (Lenore Zuck, University of Illinois, Chicago)An optimizing compiler is commonly structured as a sequence of passes each transforming a source program into a target one. The proof that a such a transformation pass is correct consists of a relation between source and target, often with the aid of invariants. Those invariants also enable further optimizations. Thus, the two tasks of proving the validity of a transformation and propagating invariants to enable further optimizations are closely related. The two can be addressed by augmenting each transformation with A witness — a stuttering simulation relation between the target and source programs which guarantees correctness for that pass. This stuttering simulation relation forms a sound and complete witness format. Witnesses can be generated either automatically or by (sound) external static analyzers. The talk will describe both witness generation and witness propagation, and demonstrate the feasibility of the approach on the LLVM compiler. Each optimization pass is augmented with a witness generator. This allows to construct an independent translation validation framework for the compiler as well as to generate an independent verification for each of its runs. The automatically generated invariants, as well as some obtained by Frama-C, can then propagated to enhance optimizations. This is demonstrated on experiments where propagated witnesses are used to substantially improve the effectiveness of several optimizations. -
10 Apr 2017 at 12:00 in room 4523, Lindstedtsvägen 5
**Complexity results in automated planning** (Meysam Aghighi, Linköping University)Planning is the problem of finding a sequence of actions that achieve a specific goal from an initial state. This problem is computationally hard in the general case. Propositional planning is PSPACE-complete and first-order planning is undecidable. Cost-optimal planning (COP) is a type of planning where each action has a cost and the goal is to find a satisfying plan with minimal cost. We show how under different restrictions, COP varies from being polynomial-time solvable to PSPACE-complete. Net-benefit planning (NBP) is a type of planning where the goal is to find a plan that maximizes the achieved utility minus the cost spent. We present a method for efficiently compiling NBP into the ordinary plan existence problem. We also show the effect of numeric domains for action costs in COP using parameterized complexity. Planning is PSPACE-complete regardless of whether action costs are positive or non-negative, integer or rational. We distinguish between these cases and show that COP is W[2]-complete for positive integer costs, but it is para-NP-hard if the costs are non-negative integers or positive rationals. -
27 Mar 2017 at 12:00 in room 4523, Lindstedtsvägen 5
**Complexity theory beyond deterministic exponential time and applications** (Igor Carboni Oliveira, Charles University)In the first part of the talk, I'll survey a variety of connections between non-uniform circuit lower bounds, non-trivial proof systems, non-trivial learning algorithms, and variants of natural properties. In particular, I plan to discuss how one can prove new unconditional lower bounds for standard complexity classes such as REXP, ZPEXP, BPEXP, and NEXP by designing algorithms with a non-trivial running time. After the break, we will focus on a recent application of some of the complexity-theoretic techniques behind these results. I'll describe in more detail recent progress on the problem of efficiently generating large canonical prime numbers, via pseudodeterministic pseudorandomness. If there is enough time and interest, I'll also discuss some non-constructive aspects of the result, and connections to derandomization. Based on joint work with Rahul Santhanam. -
20 Mar 2017 at 13:15 in Biblioteket 1440, Lindstedtsvägen 3
**Logical modelling, specification, verification and synthesis of multi-agent systems: an introduction** (Valentin Goranko, Stockholm University)In this talk I will introduce concurrent game models for multi-agent systems and the Alternating-time temporal logic ATL as the currently most popular logical system for formalizing and reasoning about strategic abilities in such systems. I will illustrate the semantics of ATL with some examples and will discuss briefly the logical decision problems of model checking and constructive satisfiability testing of ATL formulae, and how these can be used for specification, verification, and synthesis of concurrent game models. -
16 Mar 2017 at 13:15 in room 4523, Lindstedtsvägen 5
**Dag-like communication and its application** (Dmitry Sokolov, St. Petersburg Department of V. A. Steklov Institute of Mathematics)n this talk we consider a generalization of communication protocols to dag-like case (instead of classical one where protocols correspond to trees). We prove an analogue of Karchmer-Wigderson Theorem for this model and boolean circuits. We also consider a relation between this model and communication PLS games proposed by Razborov in 1995 and simplify the proof of Razborov's analogue of Karchmer-Wigderson Theorem for PLS games. We also consider a dag-like analogue of real-valued communication protocols and adapt a lower bound technique for monotone real circuits to prove a lower bound for these protocols. We use real-valued dag-like communication protocols to generalize ideas of "feasible interpolation" technique, which helps us to prove a lower bound on the Cutting Planes proof system (CP) and adapt it to "random CP" by using recent result of Krajíček. Our notion of dag-like communication games allows us to use a Raz-McKenzie transformation from Goos and Pitassi paper, which yields a lower bound on the real monotone circuit size for the CSPSAT problem. -
15 Mar 2017 at 10:00 in roon 4523
**On polynomial approximations to AC0** (Prahladh Harsha, Tata Institute of Fundamental Research)In this talk, we will discuss some questions related to polynomial approximations of AC0. A classic result due to Tarui (1991) and Beigel, Reingold, and Spielman (1991), states that any AC0 circuit of size s and depth d has an ε-error probabilistic polynomial over the reals of degree at most (log(s/ε))^{O(d)}. We will have a re-look at this construction and show how to improve the bound to (log s)^{O(d)}⋅log(1/ε), which is much better for small values of ε. As an application of this result, we show that (log s)^{O(d)}⋅log(1/ε)-wise independence fools AC0, improving on Tal's strengthening of Braverman's theorem that (log(s/ε))^{O(d)}-wise independence fools AC0. Time permitting, we will also discuss some lower bounds on the best polynomial approximations to AC0. -
13 Mar 2017 at 12:00 in room 4523, Lindstedtsvägen 5
**A nearly tight sum-of-squares lower bound for the planted clique problem** (Aaron Potechin, Institute for Advanced Study)The sum of squares (SoS) hierarchy, a method for deciding the feasibility of polynomial equations over the reals, is an exciting frontier of complexity theory. SoS is exciting because it can be applied to a wide variety of combinatorial optimization problems and is in fact conjectured to be optimal for many important problems. However, its performance is only partially understood. In this talk, I will describe recent work proving sum of squares lower bounds for the planted clique problem, a classic average case problem. In the first part of the talk, I will describe the sum of squares hierarchy, planted clique, and pseudo-calibration, a key idea for the lower bound. In the second part of the talk, I will describe the main technical ideas needed in the proof. -
06 Mar 2017 at 13:15 in room 4523, Lindstedtsvägen 5
**SAT-based learning to verify liveness of randomised parameterised systems** (Philipp Rümmer, Uppsala University)We consider the problem of verifying liveness for systems with a finite, but unbounded, number of processes, commonly known as parameterised systems. Typical examples of such systems include distributed protocols (e.g. for the dining philosopher problem). Unlike the case of verifying safety, proving liveness is still considered extremely challenging, especially in the presence of randomness in the system. We introduce an automatic method of proving liveness for randomised parameterised systems under arbitrary schedulers. Viewing liveness as a two-player reachability game (between Scheduler and Process), our method is a CEGAR approach that synthesises a progress relation for Process that can be symbolically represented as a finite-state automaton. The method constructs a progress relation by means of a suitable Boolean encoding and incremental SAT solving. Our experiments show that our algorithm is able to prove liveness automatically for well-known randomised distributed protocols, including Lehmann-Rabin Randomised Dining Philosopher Protocol and randomised self-stabilising protocols (such as the Israeli-Jalfon Protocol). To the best of our knowledge, this is the first fully-automatic method that can prove liveness for randomised protocols. -
25 Jan 2017 at 10:00 in room 4523,, Lindstedtsvägen 5
**The State of the Art of Automatic Program Repair** (Martin Monperrus, University of Lille & INRIA France)Automatic software repair is the process of fixing software bugs automatically and is a very active research area. Before having a large impact on practice, current research tries to understand the fundamental strengths and weaknesses of the best-of-breed repair algorithms. This talk presents the results of a recent experiment on repairing 224 real Java bugs from open source projects. Ref: Automatic Repair of Real Bugs in Java: A Large-Scale Experiment on the Defects4J Dataset (Matias Martinez, Thomas Durieux, Romain Sommerard, Jifeng Xuan and Martin Monperrus), In Springer Empirical Software Engineering, 2016. Nopol: Automatic Repair of Conditional Statement Bugs in Java Programs (Jifeng Xuan, Matias Martinez, Favio DeMarco, Maxime Clément, Sebastian Lamelas, Thomas Durieux, Daniel Le Berre and Martin Monperrus), In IEEE Transactions on Software Engineering, 2016. -
23 Jan 2017 at 12:00 in room 4523, Lindstedtsvägen 5
**Cumulative space in black-white pebbling and resolution** (Susanna F. de Rezende, Theory Group, KTH)The space usage of a computation is usually defined as the maximum memory it requires, and this is essentially everything one would want to know if the computational model is static. But what if we are computing in an environment where we can allocate memory dynamically? Then it makes a big difference whether we only have one single spike of high memory consumption or whether we consistently need large amounts of memory throughout the whole computation. In this talk we will explore a complexity measure, namely cumulative space, which allows us to measure this difference by accounting for the sum of memory usage over all time steps rather than just the maximum. It was introduced for pebble games by [Alwen and Serbinenko '15] and used to propose a more robust definition of cryptographic functions that are hard to invert (memory-hard functions). We will present some results regarding the cumulative space of another pebble game, namely the black-white pebble game, and relate this to the cumulative space complexity of refuting formulas in the resolution proof system. This is joint work with Joël Alwen, Jakob Nordström and Marc Vinyals. This presentation will also serve as Susanna's 50% PhD ladder seminar. -
18 Jan 2017 at 12:00 in room 1537, Lindstedtsvägen 3
**The QRAT proof system** (Martina Seidl, Johannes Kepler University Linz)We present QRAT, a novel proof system for quantified Boolean formulas. With QRAT it is now possible to produce certificates for all reasoning techniques implemented in state-of-the-art QBF preprocessors. Such certificates are not only useful to efficiently validate the correctness of a result, but they also allow the extraction of Skolem functions, i.e., winning strategies for satisfiable formula instances. In this talk, we first introduce the rules of QRAT, then we show how they can be used to express some powerful reasoning techniques implemented in modern preprocessors, and finally we outline how to extract a Skolem function from a QRAT proof.
Previous years' seminars. |