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

  • 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 campus-based 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.

  • 27 Feb 2019 at 13:15 in 4523
    Cutting Planes in Pseudo-Boolean SAT Solving
    (Stephan Gocht)

    Modern conflict-driven 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 pseudo-Boolean (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 release-acquire semantics
    (Tuan Phong Ngo)

    We present a framework for the efficient application of stateless model checking to concurrent programs running under the Release-Acquire 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 read-from 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 read-from relation, we avoid a potentially significant source of redundancy.

    Our framework is based on a novel technique for determining whether a particular read-from relation is feasible under the Release-Acquire semantics. We define a stateless model checking algorithm which is provably optimal in the sense that it explores each program order and read-from 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 state-of-the-art tools that can handle the Release-Acquire 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)


    - Lunch is served at 12:00 noon (register at 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 (x-d, 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 (x-d, 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 zero-sum turn-based 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 real-life 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 co-authors for perfect information case and LTL objectives under two settings: cooperative and non-cooperative.

    We first study the computational complexity of the rational synthesis problems (in turn-based and concurrent setting) and provide tight results for most of the classical omega-regular 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 zero-sum turn-based 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.