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.
TCS Seminar Series Autumn 2018
10 Oct 2018 at 11:15 in Room 1537
Concurrent Determinism Using Lattices and the Object Capability Model
Parallelization is an important part of modern data systems. However, the non-determinism of thread scheduling introduces the difficult problem of considering all different execution orders when constructing an algorithm. Therefore deterministic-by-design concurrent systems are attractive. A new approach called LVars consists of using data which is part of a lattice, with a predefined join operation. Updates to shared data are carried out using the join operation and thus the updates commute. Together with limiting the reads of shared data, this guarantees a deterministic result. The Reactive Async framework follows a similar approach but has several aspects which can cause a non-deterministic result. The goal with this thesis is to explore how we can amend Reactive Async in order to guarantee a deterministic result. First an exploration into the subtleties of lattice based data combined with concurrency is made. Then a formal model based on a simple object-oriented language is constructed. The constructed small-step operational semantics and type system are shown to guarantee a form of determinism. This shows that LVars-similar system can be implemented in an object-oriented setting. Furthermore the work can act as a basis for future revisions of Reactive Async and similar frameworks.
09 Oct 2018 at 13:15 in Room 4523
Hoare Logic Contracts in Denotational Semantics
(Dilian Gurov, KTH)
We sketch a simple theory of Hoare logic contracts for programs with procedures, presented in denotational semantics. In particular, we give a simple semantic justification of the usual procedure-modular treatment of such programs. The justification is given by means of a proof of soundness of a contract-relative denotational semantics against the standard denotational semantics of procedures in the context of procedure declarations. The suggested formal development can be used as an inspiration for more ambitious contract theories.
02 Oct 2018 at 13:15 in 4523
Behavioral Changes Detection with Test Amplification
With the rise of the DevOps and Continuous Integration, pull request based development is becoming a trendy way for developers to avoid breaking an existing part of the application while it evolves. To do this, developers use several tools and approaches: test selection to detect regression, the evolution of code coverage and so on. However, the existing test suite might fail to encode the behavioral changes introduced by the proposed patch. In this paper, we propose to explore an automatic way to obtain test methods that characterize behavioral changes of a patch, i.e. the behavioral difference between two versions of the same program can be encoded by test methods that pass on a given version but fail on the other one. This approach is a toolchain based on test suite amplification and is meant to be exploited by the Continuous Integration. We study real applications from GitHub to ensure the applicability and the scalability of the approach.
01 Oct 2018 at 13:15 in 4523
The Essence of Similarity in Redundancy-based Program Repair
Recently, there have been original attempts to use the concept of similarity in program repair. Given that those works report impressive results in terms of repair effectiveness, it is clear that similarity has an important role in the repair process. However, there is no dedicated work to characterize and quantify the role of similarity in redundancy-based program repair. This is where our paper makes a major contribution, we perform a deep and systematic analysis of the role of similarity during the exploration of the repair search space. We show that with similarity analysis, only 0.65% of the search space (on average over 2766 bugs) must be explored before finding the correct patch. And it is capable of ranking the correct ingredient first in the most of the time (65%).
18 Sep 2018 at 11:00 in Room 4523
How can the Eclipse Foundation help you promote your research in open source
(Gaël Blondelle, Eclipse Europe)
Eclipse has been famous for the last 17 years for the Eclipse IDE. But nowadays, the Eclipse Foundation hosts more than 350 projects in very different domains, some related to the Eclipse platform like the Eclipse Modeling stack, other focused on other domains like the IoT Working Group. With Java EE migrating to the Eclipse Foundation under the name of Jakarta EE, that’s a whole new ecosystem for enterprise Java that joins the ecosystem. Since 2013, the Eclipse Foundation Europe has been a partner of several European research projects, with the main mission to help the partners create an open source community to foster dissemination and make the results sustainable. This presentation will quickly introduce the principles of the Eclipse ecosystem, the technology landscape of the Eclipse Foundation, and how the Eclipse Foundation helps universities in Europe to publish their research results in open source.
17 Sep 2018 at 13:45 in 4523
Comparing Risk Identification in Hazard Analysis and Threat Analysis
(Hideaki Nishihara, AIST)
In the context of cyber-physical systems, safety and security have been discussed and dealt with separately in the past, since security was not a critical issue of safety and vice versa. They are similar in some points, and it is natural to try dealing with them in parallel or in a uni ed manner. This talk considers symmetrical treatment of safety and security, especially in identifying possible harms. We compare the result of hazard analysis and threat analysis for a single model of a small IoT system. It shows that identfied harms have much overlaps, which indicates the two analyses can be unified.
17 Sep 2018 at 13:15 in 4523
Optimal Test Suite Generation for Modified Condition Decision Coverage using SAT solving
(Takashi Kitamura, AIST)
Boolean expressions occur frequently in descriptions of com- puter systems, but they tend to be complex and error-prone in complex systems. The modified condition decision coverage (MCDC) criterion in system testing is an important testing technique for Boolean expression, as its usage mandated by safety standards such as DO-178  (avionics) and ISO26262  (automotive). In this paper, we develop an algorithm to generate optimal MCDC test suites for Boolean expressions. Our algo- rithm is based on SAT solving and generates minimal MCDC test suites. Experiments on a real-world avionics system confirm that the technique can construct minimal MCDC test suites within reasonable times, and improves significantly upon prior techniques.
13 Sep 2018 at 13:15 in Room 4523
Security and Quality Assurance for Deep Learning System
Over the past decades, deep learning (DL) systems achived tremendous success and gained great popularity in various applications, e.g., robotics, image processing, speech processing, and medical diagnostics. A deep neural network (DNN), as a type of deep learning systems, is the key driving force behind its recent success. However, the security and quality assurance techniques for DL are still as the early stage, and a plethora of studies have shown that the state-of-the-art DL systems suffer from various vulnerabilities which can lead to severe consequences when applied to real-world applications. In this talk, we will touch the current state-of-the art and discuss our ongoing work towards proposing general purpose security and quality assurance technique for DL systems.
12 Sep 2018 at 10:00 in 4523, Lindstedtsvägen 5
From Runtime Failures to Patches: Study of Patch Generation in Production
(Thomas Durieux, Inria, http://durieux.me/)
This presentation presents two new patch generation techniques that aim to remove the human intervention for patch generation. The core idea of these two techniques is to put as close as possible the patch generation to the production environment. The production environment contains the data and executions that can be analyzed to understand the behavior of the application and identify the bugs. This presentation presents our approaches to exploit this information to create patches for client and server-side applications.
Previous years' seminars.