TCS Seminar Series
Please tell Stephan Gocht 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 other seminars, such as our in depth Theory reading group.
TCS Seminar Series Spring 2019

27 May 2019 at 13:15 in 4523, Lindstedtsvägen 5
Automated Approaches for Formal Verification of Simulink Models
(Predrag Filipovikj, Mälardalen University)Simulink is the de facto standard modelbaseddevelopment environment in many domains such as the automotive domain, avionics domain, railways domain, etc. For quality assurance of the Simulink models the industrial stateofpractice resorts to simulation, which gives insight in the system's behavior, yet does not provide a high degree of assurance that the model behaves correctly. With the everincreasing size and complexity, as well as safety relevance of the software functions developed in Simulink, the industry has an imperative need for automated and mathematicallyrigorous approaches for verification of Simulink models, which provide higher degree of confidence of the verification result.

20 May 2019 at 14:15 in 4523, Lindstedtsvägen 5  floor 5
Recent Progress in Distributed Edge Connectivity
(Mohit Daga)In this talk, we present an overview of our recent result in distributed edge connectivity. In particular, we present the first sublineartime algorithm for finding edge connectivity k in CONGEST model as long as there are no parallel edges. Our algorithm takes O(n^{11/353}D^{1/353}+n^{11/706}) time to compute k and a cut of cardinality k with high probability, where n and D are the number of nodes and the diameter of the network, respectively. This running time is sublinear in n (i.e. O(n^{1\epsilon})) whenever D is.
This is joint work with Monika Henzinger, Danupon Nanongkai and Thatchaphol Saranurak. This talk will count as Mohits 30% seminar.

08 May 2019 at 14:15 in 4523
Breaking Quadratic Time for Small Vertex Connectivity
(Thatchaphol Saranurak) 
06 May 2019 at 13:15 in 4523, Lindstedtsvägen 5  floor 5
Coming: a Tool for Mining Change Pattern Instances from Git Commits
(Matias Sebastian Martinez, Université Polytechnique HautsdeFrance (France))Software repositories such as Git have become a relevant source of information for software engineer researchers. For instance, the detection of commits that fulfill a given criterion (e.g., bugfixing commits) is one of the most frequent tasks done to understand the software evolution. However, to our knowledge, there is no opensource tool that, given a Git repository, returns all the instances of a given code change pattern. In this talk, I will present Coming, a tool that takes as input a Git repository and mines instances of code change patterns present on each commit. For that, Coming computes finegrained code changes between two consecutive revisions, analyzes those changes to determine if they correspond to an instance of a change pattern (specified by the user using XML), and finally, after analyzing all the commits, it presents a) the frequency of code changes and b) the instances found in each commit.

29 Apr 2019 at 12:00 in 4523, Lindstedtsvägen 5  floor 5
Extended Formulation Lower Bounds for Refuting Random CSPs
(Jonah BrownCohen)PRACTICALITIES
Lunch is served at 12:00 noon (register at http://www.csc.kth.se/tcs/seminars/lunch/20190329 at the latest the Saturday before, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for 1½2 hours of more technical discussions.
There will be a more detailed technical discussionafter the seminar.
ABSTRACT
Random constraint satisfaction problems (CSPs) such as random 3SAT are conjectured to be computationally intractable. The average case hardness of random 3SAT and other CSPs has broad and farreaching implications for problems in approximation, learning theory and cryptography. In many cases, the best known algorithms for CSPs come from linear or semidefinite programs, so a natural question is to prove lower bounds on the size of such programs for random CSPs.
In this talk, we will give subexponential lower bounds on the size of linear programming extended formulations for refuting random instances of constraint satisfaction problems. In particular, our results imply that any LP extended formulation that refutes a constant fraction of random kSAT instances (with constant clause density) must have size exponential in n^{1  2/k}.
We use the technique of pseudocalibration to directly obtain extended formulation lower bounds from the distribution on instances with a planted satisfying assignment. This approach bypasses the need to construct SheraliAdams integrality gaps in proving general LP extended formulation lower bounds. As a corollary, we obtain a selfcontained proof of subexponential SheraliAdams LP lower bounds for these problems.

25 Apr 2019 at 13:15 in 4523, Lindstedtsvägen 5  floor 5
Highdimensional estimation via sumofsquares proofs
(David Steurer)Estimation is the computational task of approximately recovering a hidden parameter x associated with a distribution D_x given a draw y from the distribution D_x. Numerous interesting questions in statistics, machine learning, and signal processing are captured in this way, for example, sparse linear regression, Gaussian mixture models, topic models, and stochastic block models.
In many cases, there is currently a large gap between the statistical guarantees of computationally efficient algorithms and the guarantees of computationally inefficient methods; it is an open question if this gap is inherent in these cases or if better computationally efficient estimation algorithms exist.
In this talk, I will present a metaalgorithm for estimation problems based on the sumofsquares method of Shor, Parrilo, and Lasserre. For some problems, e.g., learning mixtures of spherical Gaussians, this metaalgorithm is able to close previous longstanding gaps and achieve nearly optimal statistical guarantees. Furthermore, it is plausible that, for a wide range of estimation problems, the statistical guarantees that this metaalgorithm achieves are best possible among all efficient algorithms.
This talk is based on an ICM proceedings article with Prasad Raghavendra and Tselil Schramm.
Coauthors: Prasad Raghavendra and Tselil Schramm

11 Apr 2019 at 13:15 in Room 1625, Lindstedtsvägen 3  floor 6
Distributed system development with ScalaLoci
(Guido Salvaneschi, Assistant Professor, TU Darmstadt, Germany)Distributed applications are traditionally developed as separate modules, often in different languages, which react to events, like user input, and in turn produce new events for the other modules. Separation into components requires timeconsuming integration. Manual implementation of communication forces programmers to deal with lowlevel details. The combination of the two results in obscure distributed data flows scattered among multiple modules, hindering reasoning about the system as a whole.
The ScalaLoci distributed programming language addresses these issues with a coherent model based on placement types that enables reasoning about distributed data flows, supporting multiple software architectures via dedicated language features and abstracting over lowlevel communication details and data conversions. As we show, ScalaLoci simplifies developing distributed systems, reduces errorprone communication code and favors early detection of bugs.

28 Mar 2019 at 13:15 in 1625, Lindstedtsvägen 3
Industrial Continuous Integration (CI) environment for 5G Radio at Ericsson
(Han Fu)A worldclass Continuous Integration (CI) machinery using state of the art technology is one of the key enablers for Ericsson to have faster, more, better 5G radio product deliveries to our customers. In order to achieve that, we build up a fully automated CI loop for fully 5G Radio functional test. One delivery of 5G Radio software can be an hourly base. In this session, the elaborate setup of Ericsson Radio Software CI loop will be introduced, along with the intricacy setup of Radio test tower for functional test purpose. Furthermore, in our future work, we see an inspiring opportunity for Ericsson to leverage and extend ongoing most advanced research in AIdriven programrepair to drastically reduce system development cost.

26 Mar 2019 at 11:15 in 1537, Lindstedtsvägen 3  floor 5
Machine Learning for Large Scale Code Analysis
(Hugo Mougard)"Software is eating the world". Yet, applying Machine Learning techniques to code is challenging: to fully take advantage of its structured nature requires clever models, and to fully take advantage of the enormous quantities of code available requires precise engineering. We'll see in this talk how the Machine Learning team at source{d} leverages a stack to transform code as a first class citizen in Machine Learning to deliver insight on code. We'll then focus on one of its latest experiments: a model to fix formatting mistakes in code.

11 Mar 2019 at 12:00 in 4523, Lindstedtsvägen 5  floor 5
Some new applications of Razborov's pseudowidth method
(Kilian Risse)PRACTICALITIES
Lunch is served at 12:00 noon (register at http://www.csc.kth.se/tcs/seminars/lunch/20190311 at the latest the Saturday before, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for 1½2 hours of more technical discussions.
There will be a more detailed technical discussionafter the seminar. This is Kilian's 30% seminar.
ABSTRACT
Resolution is arguably the most wellstudied proof system for certifying unsatisfiability of Boolean formulas. The sizewidth bound in the celebrated paper by BenSasson and Wigderson shows that for resolution proofs linear lower bounds on the width, measured in the number of variables, imply exponential size lower bounds. This method does not extend to formulas where such strong width lower bounds are simply not true  e.g., for the so called weak pigeonhole principle formulas claiming that m pigeons can be mapped onetoone to n holes for m >> n. In a breakthrough result in 2001 Raz proved exponential size lower bounds for such formulas, which Razborov subsequently strengthened and generalized with his socalled pseudowidth method developed in a series of papers. In this seminar we discuss this framework and show how to generalize it further in order to obtain size lower bounds for other formulas. This seminar is based on joint work with Susanna F. de Rezende, Jakob Nordström and Dmitry Sokolov.

06 Mar 2019 at 09:00 in 4523, Lindstedtsvägen 5, floor 5
Experiences and use of assessment in introductory computer science
(Emma Riese)As teachers, we can use assessment as a way to guide the students to the most important parts of the course material and to provide feedback on the students’ progress. How the assessment is planned and carried out can, therefore, be said to influence the students’ learning. Understanding students’, TAs’ and teachers’ experiences and use of the assessment could give us insights into how to further improve our courses in order to enhance learning among our students. During this seminar, Emma will give a brief background to her research and present two of her conducted studies. Both studies had a focus on experiences, but from different aspects and in different contexts. The first study uses a phenomenographic approach to categorize students' experiences of assessment throughout an online course. The second study, identified themes in how TAs experience their role and responsibilities in the context of lab sessions in campusbased introductory computer science courses. Emma will also present her ongoing research project about TAs and assessment, as well as her ideas for future studies to build on the presented results towards a thesis.
Emma Riese is a PhD student at KTH, now giving her 50% seminar. Prof. Arnold Pears from the Department of Learning in Engineering Sciences, ITM school, will act as the opponent during the seminar.

04 Mar 2019 at 13:15 in 4523, Lindstedtsvägen 5  floor 5
Extending finitememory determinacy by Boolean combination of winning conditions
(Stephane Le Roux, LSV Cachan)We study finitememory (FM) determinacy in games on finite graphs, a central question for applications in controller synthesis, as FM strategies correspond to implementable controllers. We establish general conditions under which FM strategies suffice to play optimally, even in a broad multiobjective setting. We show that our framework encompasses important classes of games from the literature, and permits to go further, using a unified approach. While such an approach cannot match adhoc proofs with regard to tightness of memory bounds, it has two advantages: first, it gives a widelyapplicable criterion for FM determinacy; second, it helps to understand the cornerstones of FM determinacy, which are often hidden but common in proofs for specific (combinations of) winning conditions. This is joint work with Arno Pauly and Mickael Randour.

27 Feb 2019 at 13:15 in 4523
Cutting Planes in PseudoBoolean SAT Solving
(Stephan Gocht)Modern conflictdriven clause learning (CDCL) SAT solvers are able to solve problems with millions of variables. To achieve this, the solver must be capable of efficient reasoning. Especially, it has to be able to find a relatively short proof of unsatisfiablity if there are no solutions, as checking the exponential number of possible assignments to the variables is not feasible. Surprisingly, modern solvers are still based on Resolution, which is a rather weak form of reasoning and an extension to stronger proof systems such as cutting planes, as is done in some pseudoBoolean (PB) solvers, could in theory result in exponential improvements. However, such gains are rarely realized in practice. A possible explanation for this is that the PB solvers only use restricted versions of cutting planes that actually limit the reasoning power.
In this presentation I will give an introduction to the cutting planes proof system and show on an example how it can be used for efficient reasoning. Then we will discuss how different restrictions made in practice effect the reasoning power of cutting planes. Especially, I will present the latest results on the use of the division rule vs. the saturation rule, which is joint work with Jakob Nordström and Amir Yehudayoff.
There will be a more detailed technical discussion on how these results can be obtained after the seminar. This is Stephan's 30% seminar.

18 Feb 2019 at 13:15 in 4523, Lindstedtsvägen 5  floor 5
Optimal stateless model checking under the releaseacquire semantics
(Tuan Phong Ngo)We present a framework for the efficient application of stateless model checking to concurrent programs running under the ReleaseAcquire fragment of the C/C++11 memory model. Our approach is based on exploring the possible program orders, which define the order in which instructions of a thread are executed, and readfrom relations, which specify how reads obtain their values from writes. This is in contrast to previous approaches, which also explore the possible coherence orders, i.e., orderings between conflicting writes. Since unexpected test results such as program crashes or assertion violations depend only on the readfrom relation, we avoid a potentially significant source of redundancy.
Our framework is based on a novel technique for determining whether a particular readfrom relation is feasible under the ReleaseAcquire semantics. We define a stateless model checking algorithm which is provably optimal in the sense that it explores each program order and readfrom relation exactly once. This optimality result is strictly stronger than previous analogous optimality results, which also take coherence order into account. We have implemented our framework in the tool Tracer. Experiments show that Tracer can be significantly faster than stateoftheart tools that can handle the ReleaseAcquire semantics.

11 Feb 2019 at 12:00 in 4523, Lindstedtsvägen 5  floor 5
Restricted arithmetic progressions and correlated spaces in the product model.
(Jan Hązła, MIT)PRACTICALITIES
 Lunch is served at 12:00 noon (register at https://tinyurl.com/yacnb46v at the latest the Saturday before, but preferably earlier).  The presentation starts at 12:10 pm and ends at 1 pm.  Those of us who wish reconvene after a short break for 1½2 hours of more technical discussions.
ABSTRACT An arithmetic progression in F_3^n is a triple of elements (xd, x, x+d) for some d not equal to 0^n. In a recent breakthrough the polynomial method has been used to establish that a set in F_3^n that does not contain any progressions must have at most alpha^n elements for some absolute alpha < 3. It turns out that this result is equivalent to a probabilistic version: A set with mu * 3^n elements must contain at least mu^C * 9^n progressions for some absolute finite C.
I will talk about a variant of this problem where we look at restricted progressions (xd, x, x+d), where d is constrained to lie in {0, 1}^n. In this case it is known that a set that does not contain restricted progression must have at most o(1) * 3^n elements for a very slowly decaying o(1). The best known lower bound is of the form alpha^n, similar as for unrestricted progressions. The probabilistic version is even more open: It is not known if there exists any positive c(mu) such that a set with mu * 3^n elements must contain at least c(mu) * 6^n restricted progressions, and the best known lower bound is mu^C * 6^n.
I will also put this problem in a broader context, where one considers "correlated spaces": more general structures over finite alphabet Omega that are then "tensorized" in the product space Omega^n. I will talk about some open problems and partial results, including joint work with Thomas Holenstein and Elchanan Mossel.

06 Feb 2019 at 13:15 in 4523, Lindstedtsvägen 5  floor 5
Rational Synthesis
(Rodica Condurache, Department of Computer Science, “A.I.Cuza” University of Iasi, Romania.)The synthesis problem aims at automatically designing a program from a given specification. Several applications for this formal problem can be found in the design of interactive systems i.e., systems interacting with an environment. From a formal point of view, the synthesis problem is traditionally modeled as a zerosum turnbased game and then the system and the environment are modeled by two players with opposite interest. Hence, a strategy that allows the system to achieve its goal against any behavior of the environment is a winning strategy and is exactly the program to synthesize.
However, in the reallife cases, the system may be composed by several components (agents) that may not necessarily have as objective to defeat the system to synthesize and they play rationally, meaning that they first want to satisfy their objectives and then they may think to harm the others. Therefore the system to be synthesized has to fight only against rational behaviors (modeled as equilibria). This problem was introduced by Kupferman, Vardi and coauthors for perfect information case and LTL objectives under two settings: cooperative and noncooperative.
We first study the computational complexity of the rational synthesis problems (in turnbased and concurrent setting) and provide tight results for most of the classical omegaregular objectives, and show how to solve those problems optimally. The idea is to either study the existence of equilibria in the provided game, or, given an instance of the rational synthesis problem, to construct a zerosum turnbased game that can be adapted to each one of the class of objectives and then solved efficiently.

04 Feb 2019 at 13:15 in 4523, Lindstedtsvägen 5  floor 5
Cyber Situational Awareness  Aspects of gaining insights for the cyber mission
(Stefan Varga, KTH)In today’s world, organizations are heavily dependent on IT systems. Such systems may contain valuable information, but also control physical processes. System owners want to maintain a desired level of functionality, and to preserve the confidentiality and integrity of critical information. Taking the current cyber threat landscape into account, there is a need to secure networks to an adequate level.
Cyber situational awareness, CSA, is about being sufficiently well informed about factors that will influence one’s cyber mission. One example would be to uphold the security stance of an IT system. We hypothesize that the level of correct awareness to some extent corresponds to decision makers' ability to make rational choices that ultimately affect the security stance. Hence, to gain CSA, it is of importance to carefully select the underlying needed information, process it, and present it in an effective way for decision makers.
During the seminar Stefan will present the context of cyber situational awareness as well as the result of two studies. The first study used an exploratory research approach made in the form of a survey among the participants of a large national information assurance exercise. The second study was a case study that sought to examine the usefulness of a text mining tool for solving a realistic intelligence assessment task. This study was conducted in the form of an experiment with an operational unit within the Swedish Armed Forces. Stefan Varga is a PhD student at KTH, now giving his 30% seminar.

29 Jan 2019 at 10:15 in 1537, Lindstedtsvägen 3  floor 5
Program State Coverage: A Test Coverage Metric Based on Executed Program States (SANER' 19 paper)
(Khashayar Etemadi Someoliayi)In software testing, different metrics are proposed to predict and compare test suites effectiveness. In this regard, Mutation Score (MS) is one of most accurate metrics. However, calculating MS needs executing test suites many times and it is not commonly used in industry. On the other hand, Line Coverage (LC) is a widely used metric which is calculated by executing test suites only once, although it is not as accurate as MS in terms of predicting and comparing test suites effectiveness. In this paper, we propose a novel test coverage metric, called Program State Coverage (PSC), which improves the accuracy of LC. PSC works almost the same as LC and it can be calculated by executing test suites only once. However, it further considers the number of distinct program states in which each line is executed. Our experiments on 120 test suites from four packages of Apache Commons Math and Apache Commons Lang show that, compared to LC, PSC is more strongly correlated with normalized MS. As a result, we conclude that PSC is a promising test coverage metric.
Previous years' seminars.