The D3S Seminar is a regular meeting event of the department members and guest speakers. It is also a regular course Advanced Topics in Distributed and Component-Based Systems I, II (NSWI057, NSWI058). This course is recommended for Ph.D. and advanced graduate students.

Regular meetings take place on Tuesdays at 14:00 in S5 (if not noted otherwise in the schedule below).

We recommend subscribing to the seminar mailing list to receive announcements on special seminars, schedule updates and other important news.

Scheduled seminars

No seminars are currently scheduled.

Passed seminars

Jan Kofroň

September 24, 2019

Habilitation talk rehearsal

The talk will introduce the interpolation-based verification and our contribution to the area.


Rima Al-Ali

June 25, 2019

Uncertainty in Self-Adaptive Cyber-Physical Systems (last updates)

In Cyber-Physical Systems, the self-adaptation is associated with how the system perceives the surrounding environment and tunes its behavior to what serves the system requirements best. Nevertheless, the assumptions and decisions about the system in design time influence the output of the system at runtime. This leads to questioning about the suitability the assumptions and if they impact on selecting the system requirements. Therefore, our aim is to introduce a methodology to design autonomic self-adaptive Cyber-Physical Systems. It guides designers through the development process, which includes recognizing what kind of information is needed to design their uncertainty-aware components and how to represent them at architectural level so they perform the suitable adaptation at runtime.


Jan Pacovsky

May 28, 2019

Rehearsal for Master Thesis defense: Navigation of units in games using flow networks

Navigation of units in real-time strategy computer games presents a challenge when navigating a bigger group of units is required, especially through a game world that contains narrows passages. The narrow passages may cause significant delays that could be avoided by splitting the group and guiding some part of the group through alternative paths. In this talk, a solution using flow networks is proposed.


Vlastimil Dort

May 07, 2019

Reference Immutability for Dotty

Reference immutability type systems allow declaring certain object references as read-only, and guarantee that no object accessed through such references can be mutated (by changing values of its fields). There are implementations of such type systems for statically typed object-oriented programming languages such as Java or C#, using annotation processors or language extensions. The Scala programming language, and particularly the Dotty compiler, implements advanced type system features such as path dependent types, refinement types, intersection and union types. In our work in progress, we explore the possibility of encoding reference immutability in the Scala type system using these features, and extending the type checker of Dotty to enforce correct usage of read-only references.


Pavol Gál (Vistaprint)

March 26, 2019

Security threats of microservices running in the cloud

Do you want to know: What kinds of attacks can your microservice expect? Who is the most probable attacker? How can you defend against them? Why is your login page probably not secure? What are the most common security holes in microservices? Visit the Vistaprint lecture!


Miroslav Bureš (FEL ČVUT)

March 05, 2019

Automation of tests for software and IoT systems and model-driven generation of test cases


Hans Vangheluwe (University of Antwerp - Belgium)

February 19, 2019

Multi-Paradigm Modelling of Cyber-Physical Systems (MPM4CPS)

The networking of multi-physics (mechanical, electical, hydraulic, biochemical, …) with computational systems (control systems, signal processing, logical inferencing, planning, …) processes, interacting with often uncertain environments, with human actors, in a socio-economic context, leads to so-called Cyber-Physical Systems (CPS). The CPS that are engineered today are reaching a hitherto unseen level of complexity. To date, no unifying theory nor systematic design methods, techniques and tools exist for such systems. Individual (mechanical, electrical, network or software) engineering disciplines only offer partial solutions. Multi-paradigm Modelling (MPM) proposes to model every part and aspect of such complex systems explicitly, at the most appropriate level(s) of abstraction, using the most appropriate modelling formalism(s). This includes the explicit modelling of the often complex engineering workflows. In this presentation, the causes of complexity of CPS and some of the challenges of their collaborative development are introduced, leading to the need for MPM. Modular modelling language engineering, including model transformation, and the study of modelling language semantics, are used to realize MPM.


Rolf Hennicker (Ludwig Maximilian Universität Munich)

February 12, 2019

Role-based Development of Dynamically Evolving Ensembles

Ensembles are groups of active entities which collaborate to achieve certain goals. They are characterised by a highly dynamic and adaptive behaviour. Modelling software systems for ensemble execution is challenging since such applications involve complex interaction structures and dynamically changing architectures. Our approach is centered around the notion of a role such that a component can participate (possibly at the same time) in various ensembles under specific roles. In the first part of the talk we propose a development methodology starting from dynamic logic specifications of global interaction scenarios and ending with concrete, process-algebraic desciptions of local behaviours of ensemble participants. The ability of components to change roles is useful for modelling adaptive behaviour. In the second part of the the talk we propose a strategy to develop adaptive ensembles using a role-based adapatation pattern.


Rima Al-Ali

January 15, 2019

A Methodology for Handling Uncertainty in Self-Adaptive Cyber-Physical Systems

Considering uncertaitnies in self-adaptative Cyber-Physical Systems requieres from the developer to have experinse in multiple topics. For this reason, it is hard for the non-expert to decide what kind of uncecrtainies should be considered in their design and how to manage them. Therefore, the talk will present a methodology that helps the developer to accomplish this task.


Jan Pacovský

January 08, 2019

Navigation of Units in Video Games Using Flow Networks

In the real-time strategy games, an occurring issue in the navigation of bigger groups of units is their passing through narrows passages where they spent a significant amount of time. This could be avoided by splitting the group and taking parts of the whole group through alternative ways. This talk presents a solution using flow networks.


Jiří Vinárek

December 11, 2018

Deep Reinforcement Learning For Multi-Agent Domains

Reinforcement learning (RL) has been recently used for wide variety of applications (e.g. game playing, robotics, data center cooling). Such systems are usually modeled as single-agent RL problems. However, there are many domains which involve interaction between multiple agents. Using traditional RL techniques for those problems is difficult as the environment becomes non-stationary from the perspective of a single agent.In this talk I would like to introduce approach described in paper “Multi-Agent Actor-Critic for Mixed Cooperative-Competitive Environments” from Ryan Lowe et al. where authors propose a general-purpose multi-agent framework with centralized training and decentralized execution.


Filip Kliber

December 04, 2018

Runtime Checking of Privacy and Security Contracts in Dynamic Architectures

Important aspects of the IoT concept include privacy and security. There are various examples from the past, where implementation of security was insufficient, which allowed hackers to gain unauthorized access to tens of thousands of everyday objects connected to the Internet and abuse this power to paralyze the communication over the Internet. In this thesis we designed and implemented the Glinior tool that allows to define the contracts between objects or components in the application, and ensures that the communication between specified objects or components happens according to those contracts. The Glinior tool uses techniques of dynamic analysis to verify contracts defined by the user. This is done by using the JVMTI framework with combination of the ASM library for byte-code manipulation.


Dominik Škoda

November 27, 2018

Targeting Uncertainty in Smart CPS by Confidence-based Logic

Smart Cyber-Physical Systems (sCPS) are complex distributed decentralized systems of cooperating components. They typically operate in uncertain environments and thus require means for managing variability at run-time. Architectural modes have traditionally been a proven means for the runtime variability. They are easy to understand, easy to realize in resource-constrained systems and (contrary to more sophisticated methods of learning) provide an explicit specification that can be inspected and validated at design time. However, in uncertain environments (which is the case of sCPS), they tend to lack expressivity to take into account the level of uncertainty and factor it in the mode-switching logic. I will talk about a specific logic for specifying mode-switch guards (CB logic). The semantics is based on statistical tests, which is a convenient way to reason about uncertainty in the state of the environment.


Martin Blicha

November 21, 2018

Decomposing Farkas Interpolants

Interpolant is a formula that for an unsatisfiable pair of formulas A and B is implied by A and unsatisfiable with B that uses only common vocabulary of A and B. Interpolants are commonly used in model checking algorithms for over-approximation of reachable states in order to obtain candidates for inductive invariants of modelled system. If the modelling language is linear real arithmetic, interpolants can be efficiently computed from a Simplex-based refutation by applying Farkas’ lemma. However, Farkas interpolants are not always suitable for a given verification task, in some cases even causing the verification algorithm to run indefinitely. We present the notion of decomposed interpolants, a fundamental extension of the Farkas interpolants obtained by identifying and separating independent components from the interpolant structure using methods from linear algebra. We implemented our interpolation algorithm in SMT solver OpenSMT and integrated it in a model checker SALLY. We then evaluated the effect of our new algorithm on a variety of benchmarks and confirmed its usefulness.


Patrizio Pelliccione

October 16, 2018

Effective and User-friendly Specification of Multi-Robot Missions


Filip Krijt

June 20, 2018

Networking real-time multiplayer games

For multiplayer videogames, delivering an enjoyable experience requires minimizing stuttering and latency that would otherwise arise due to the underlying network infrastructure, as well as providing a line of defense against cheaters and hackers. This implies a set of architectural design decisions, some of which are obvious, some less so. This talk will provide a short overview of the problem, as well as present a common game network architecture pattern based on the Tribes series. Variants of this pattern are still used in recent big titles such as Overwatch.


Vojtěch Horký

June 05, 2018

Performance Awareness in Agile Software Development (defence rehearsal)

Broadly, agile software development is an approach where code is frequently built, tested and shipped, leading to short release cycles. Extreme version is the DevOps approach where the development, testing and deployment pipelines are merged and software is continuously tested and updated. In this context our work focuses on identifying spots where the participants should be more aware of the performance and offers approaches and tools to improve their awareness with the ultimate goal of producing better software in shorter time. In general, the awareness is raised by testing, documenting, and monitoring the performance in all phases of the development cycle.


Martin Děcký (Huawei Technologies)

May 30, 2018

Data-Centric Computing

In recent decades, the majority of mainstream computer systems we designed as CPU-centric and memory-centric. All the data that the computer processed always passed through the main memory in one way or the other and the code running on the central processor(s) manipulated the data. DMA controllers, co-processors, GPUs and intelligent NICs were used mostly as slave peripherals, although with some degree of computational acceleration and off-loading in recent years. One of the reasons for keeping the same basic architecture despite its drawbacks such as the ever-widening memory barrier (i.e. the difference between the latency of the CPU and the RAM) was arguably its conceptual simplicity. However, trends for a major change in the status quo are emerging into the mainstream. There are new non-volatile memory technologies that promise to marry the benefits of byte-addressable volatile memory and block-addressable permanent storage. Approaches such as data-centric computing and near-data processing propose to turn an ordinary computer into a distributed system where the distinction between CPU/RAM and peripherals is much more blurry than today, with the possibility to autonomously compute within and interchange data between all the hardware components. This talk presents a brief overview of the concepts and discusses consequences for the design of the software running on top of this new hardware.


Vlastimil Dort

May 29, 2018

Simplicitly: Foundations and Applications of Implicit Function Types

Understanding a program entails understanding its context; dependencies, configurations and even implementations are all forms of contexts. Modern programming languages and theorem provers offer an array of constructs to define contexts, implicitly. Scala offers implicit parameters which are used pervasively, but which cannot be abstracted over. This paper describes a generalization of implicit parameters to implicit function types, a powerful way to abstract over the context in which some piece of code is run. We provide a formalization based on bidirectional type-checking that closely follows the semantics implemented by the Scala compiler.To demonstrate their range of abstraction capabilities, we present several applications that make use of implicit function types. We show how to encode the builder pattern, tagless interpreters, reader and free monads and we assess the performance of the monadic structures presented.


Andrea Parri

May 23, 2018

Frightening small children and disconcerting grown-ups: Concurrency in the Linux kernel

Concurrency in the Linux kernel can be a contentious topic. The Linux kernel mailing list features numerous discussions related to consistency models, including those of the more than 20 CPU architectures supported by the kernel and that of the kernel itself. How are Linux programs supposed to behave? Do they behave correctly on exotic hardware? A formal model can help address such questions. Better yet, an executable model allows programmers to experiment with the model to develop their intuition. In this talk, we discuss a formal model for the Linux kernel, written in the Cat language and executable by the Herd simulator, its design principles and its validation, with particular focus on the Read-Copy-Update synchronisation mechanism.


Vladimír Matěna

May 22, 2018

Performance Modelling of Smart Cyber-Physical Systems

Context: the dynamic nature of complex Cyber-Physical Systems (CPS) introduces new research challenges since they need to smartly self-adapt to changing situations in their environment. This triggers the usage of methodologies that keep track of changes and raise alarms whether extra-functional requirements (e.g., safety, reliability, performance) are violated. Objective: this paper investigates the usage of software performance engineering techniques as support to provide a model-based performance evaluation of smart CPS. The goal is to understand at which extent performance models, specifically Queueing Networks (QN), are suitable to represent these dynamic scenarios. Method and Results: we evaluate the performance characteristics of a smart parking application where cars need to communicate with hot-spots to find an empty spot to park. Through QN we are able to efficiently derive performance predictions that are compared with long-run simulations, and the relative error of model-based analysis results is no larger than 10% when transient or congestion states are discarded. Conclusion: the usage of performance models is promising in this domain and our goal is to experiment further performance models in other CPS case studies to assess their effectiveness.


Rima Al Ali

May 15, 2018

Generalizing Uncertainty Across Domains in Industrial Cyber-Physical Systems

Cyber-physical systems (CPS) need to be designed to deal with various forms of uncertainty associated with data contributing to the system’s knowledge of the environment. Dealing with uncertainty requires adopting an appropriate model which then allows making the right decisions and carrying out the right actions (possibly affecting the environment) based on imperfect information. However, choosing and incorporating a suitable model into CPS design is difficult, especially for non-experts, because it requires identifying the kind of uncertainty at hand as well as knowledge of suitable models and their applications. While inspiration can be found in other CPS designs, the details of dealing with uncertainty in another CPS can be confounded by domain-specific terminology, context, and requirements. To make this aspect of CPS design less daunting for non-experts, we aim at providing a generalized view of approaches dealing with uncertainty in the design of CPS targeting collective behavior. To this end, we present a systematic review of relevant projects and a synthesis of relations between system features, the kinds of uncertainty, and models and methods used to deal with it. The resulting model provides a generalized view of uncertainty across different domains and challenges.


Natalia Cantavella Franch (Erasmus student)

May 09, 2018

Smart Home in VDM

A smart home is a residence that uses internet-connected devices to enable the remote monitoring and management of appliances and systems, such as lighting and heating. In this talk, details of a student work in this area will be presented.


Iuliana Bocicor (Babeş-Bolyai University, Romania)

May 02, 2018

Python for Data Analysis

Artificial Intelligence and Machine Learning (ML) applications are ubiquitous and actively change so many aspects of our lives nowadays. One of the most used programming languages for machine learning applications is Python. Due to its simplicity and elegance, but mostly to its powerful numerical linear algebra and scientific computing libraries, Python is easy to use and thus many popular libraries that are widely used for ML tasks are written in Python. This talk describes how Python’s ML libraries can be employed for various ML tasks, with applications in medical data analysis and classification, as well as for studies and analyses on molecular biology data (DNA classification and protein dynamics).


Martin Blicha

April 24, 2018

Abstractions and refinements in bounded model checking of software

Assertions in a code can be viewed as specifications of safety properties for the program. In the context of bounded model checking, the bounded program with an assertion can be encoded as a logical formula where a safety violation corresponds to a satisfiable assignment of the formula. Traditionally, encoding to propositional logic was used to obtain a precise model of the program. To achieve better scalability, more abstract modelling languages can be used, such as logic of equality with uninterpreted functions or linear arithmetic. As a second, orthogonal, abstraction in an incremental scenario, function summaries obtained from previous successful verification runs can be used. With abstraction introduced, the counter-examples to safety found could be spurious. In case of a spurious counter-example, the abstractions need to be refined to eliminate it. Different refinement strategies can be employed and may be beneficial for different types of programs.


Dominik Škoda

April 18, 2018

Decentrally Coordinated Execution of Adaptations in Distributed Self-Adaptive Software Systems

Software systems in domains like Smart Cities, the Internet of Things or autonomous cars are coined by a high degree of distribution across several independent computing devices and the requirement to be able to adjust themselves to varying situations in their operational environment. Self-adaptive software systems are a natural choice to implement such context-dependent software systems. A multitude of approaches already implement self-adaptive systems and some consider even distribution aspects. Yet, none of the existing solutions supports the coordination of adaptation operations spanning multiple independent nodes, which is necessary to ensure a consistent adaptation even in presence of network errors or node failures. This paper, tackle this challenge to execute adaptations in distributed self-adaptive software systems in a coordinated manner. It presents a protocol that enables the self-adaptive software system to execute correlated adaptations on multiple nodes in a transactional manner ensuring an atomic and consistent transition of the distributed system from its source to the desired target configuration. The protocol is validated to be free of deadlocks for any given adaptation at any point in time using a model-checking approach. The performance of the approach is investigated in experiments that emulate the protocol’s execution on real devices for different sizes of distributed applications and adaptation scenarios.


Jiří Vinárek

April 17, 2018

Recent developments in (multi)agent deep reinforcement learning

Reinforcement learning is a kind of machine learning where an agent learns its ideal behavior without prior training data, purely via trial and error. Although the underlying concepts are not new, just recently they have been significantly improved by incorporation of deep neural networks. The talk will describe principles used in deep reinforcement learning, state-of-the art algorithms and their application to agent systems.


Etienne Borde (CNRS/Telecom ParisTech)

April 11, 2018

Timing and Availability Analysis of Mixed-Criticality Dependent Tasks with AADL

In safety-critical systems, scheduling real-time tasks on multi-core architectures raises important challenges. This talk will start with an explanation of these challenges and existing solutions focusing on mixed-criticality systems: systems in which functions of different criticality share execution resources. I will then introduce a complementary view point on mixed-criticality systems, dealing with availability of lower criticality functions. This will lead to present a task model with a representation of dependencies among tasks. Scheduling dependent tasks with different criticality levels on multicore processor has received little contributions, but I will present our recent results on this topic. AADL model transformations in the RAMSES (Refinement of AADL Models for the Synthesis of Embedded Systems) platform will enable to illustrate step by step these solutions.


Dominique Blouin (Telecom ParisTech)

April 10, 2018

Model Transformations and Management for Complex Systems Design with AADL and RAMSES

Developing complex embedded and cyber-physical systems with models makes intensive use of model transformations, model analysis and model management in order to ensure that the interplay between the models is managed properly, in addition to the activities on each individual model. Traditional model management approaches do not scale for current industrial settings made of large ecosystems of models and making use of rich languages such as the SAE Architecture Analysis and Design Language (AADL). In particular, current model transformations tools yet do not deliver appropriate performances in such context. In this talk, I will introduce our model-based engineering work with the AADL including automated code generation with our tool RAMSES (Refinement of AADL Models for the Synthesis of Embedded Systems). I will then present current scalability and model management issues and our agenda to tackle them based on incremental model transformations and synchronizations and megamodeling.


Petr Kubát

March 28, 2018

Adaptive Dispatch: A Pattern for Performance-Aware Software Self-Adaptation (WOSP-C’18 rehearsal)

Modern software systems often employ dynamic adaptation to runtime conditions in some parts of their functionality – well known examples range from autotuning of computing kernels through adaptive battery saving strategies of mobile applications to dynamic load balancing and failover functionality in computing clouds. Typically, the implementation of these features is problem-specific – a particular autotuner, a particular load balancer, and so on – and enjoys little support from the implementation environment beyond standard programming constructs. In this work, we propose Adaptive Dispatch as a generic coding pattern for implementing dynamic adaptation. We believe that such pattern can make the implementation of dynamic adaptation features better in multiple aspects – an explicit adaptation construct makes the presence of adaptation easily visible to programmers, lends itself to manipulation with development tools, and facilitates coordination of adaptation behavior at runtime. We present an implementation of the Adaptive Dispatch pattern as an internal DSL in Scala.


Oracle Researchers

January 18, 2018

Database Programming – From Active Databases via NoSQL to Cloud Computing

Introduction into database-side programming. How to do it? Discuss the challenges of effective/efficient implementation and integration with modern programming languages.


Oracle Researchers

January 17, 2018

Hack into Your Compiler!

Project Graal (JIT compiler). Implementation of Java in Java. Tour over the Graal sources, how to edit/compile/debug them. Show how to write you personal compiler.


Rima Al Ali

January 16, 2018

Handling uncertainty in self-adaptive cyber-physical systems


Oracle Researchers

January 16, 2018

Parallel Distributed Processing of Big Data,Graphs - Parallel Graph AnalytiX (PGX)

PGX.D is distributed parallel in-memory graph analysis toolkit: SQL-like pattern matching, participate on standardization of PGQL, Extreme performance of standard graph algorithms, Weakly scalable. How do we achieve all this?


Vlastimil Dort

January 10, 2018

Index Checker


Petr Kubát

January 09, 2018

Adaptive Dispatch: A Pattern for Performance-Aware Software Self-Adaptation


Jiří Vinárek

December 13, 2017

Programming robot swarms in Buzz language

One of the problems in programming of swarm robotic systems is a lack of programming primitives that would allow reusable and predictable description of a team behavior. The current practice in development of swarm systems is to either use bottom-up approach where single-robot behavior is refined until swarm-level requirements are satisfied or to use top-down approach (often used in sensor networks and spatial computing) which often has a problem with excessive simplification of the system. The talk will present the Buzz programming language from Carlo Pinciroli standing in the middle and combining advangates of the both mentioned methods.


Dominik Škoda

December 06, 2017

Situational Aware (SiA) Cyber-physical systems (CPS)

Situational Aware (SiA) Cyber-physical systems (CPS) harmoniously integrate computational and physical components to being aware of what is happening in the surroundings and using this information to decide and act. Architecture description of SiA-CPS can be a valuable tool to reason about the selected solutions, and to enable code generation and simulation. There is a paper that presents an architecture framework that automatically generates from a SiA-CPS architecture description, an executable code used to simulate the architecture model and evaluate it in terms of data traffic load, battery level and energy consumptions. The framework makes use of a model transformation approach where, three SiA-CPS domain-specific modeling views are automatically transformed into the input language of CupCarbon, an opensource tool supporting the simulation of sensor network architectures.


Grigory Fedyukovich (University of Washington)

November 29, 2017

Sampling Invariants from Frequency Distributions

Automated formal verification of programs handling unbounded loops is reduced to finding safe inductive invariants that over-approximate the sets of reachable states, but precise enough to prove unreachability of the error state. Successful solutions to this problem include Counterexample-Guided Abstraction Refinement and Property Directed Reachability, but they are not guaranteed to deliver appropriate invariants. We aim at learning inductive invariants in an “enumerate-and-check” manner, and in particular we exploit the syntactical constructions which appear in the source code to iteratively obtain partial invariants (called lemmas). We present a new SMT-based, probabilistic, syntax-guided method to discover numerical inductive invariants. The core idea is to initialize frequency distributions from the program’s source code, then repeatedly sample lemmas from those distributions, and terminate when the conjunction of learned lemmas becomes a safe invariant. The sampling process gets further optimized by priority distributions fine-tuned after each positive and negative sample. The stochastic nature of this approach admits simple, asynchronous parallelization. We present an implementation and evaluation of this approach in a tool called FreqHorn which shows competitive performance on well-known linear and some non-linear programs.


Vladimír Matěna

November 28, 2017

An Ensemble-based Approach For Scalable QoS in Highly Dynamic CPS

Modern cyber-physical systems (CPS) often involve distributed devices/components that closely interact with each other and their environment. In this context, operation conditions may constantly change and it is not always possible to guarantee quality of service (QoS), particularly, if resourcesdegrade or stop being available. In addition, sometimes, one would like QoS to scale up/down with operation conditions, e.g., maximize efficiency, minimize energy consumption, etc. without compromising safety. However, traditional design and development techniques fail to capture the dynamics of modern CPS, since they rather focus on individual components/devices, and are unable to provide such QoS guarantees. To overcome this problem, we propose a design methodology based on the concept of ensemble, i.e., a dynamic grouping of components, which allows for scalable QoS guaranties. We illustrate the utility of our approach based on a case study consisting of an intelligent production line and analyze the effect on performance as communication between components degrades. Finally, our methodology can be incorporated into existing ensemble-based tools such as DEECo, Helena or jRESP to generate executable code to be deployed onto distributed devices.


Paolo Arcaini

November 14, 2017

Automated Repairing of Variability Models

Variability models are a common means for describing the commonalities and differences in Software Product Lines (SPL); configurations of the SPL that respect the constraints imposed by the variability model define the problem space. The same variability is usually also captured in the final implementation through implementation constraints, defined in terms of preprocessor directives, build files, build-time errors, etc. Configurations satisfying the implementation constraints and producing correct (compilable) programs define the solution space. Since sometimes the variability model is defined after the implementation exists, it could wrongly assess the validity of some system configurations, i.e., it could consider acceptable some configurations (not belonging to the solution space) that do not permit to obtain a correct program. The talk presents an approach that automatically repairs variability models such that the configurations they consider valid are also part of the solution space.


Ondřej Šerý (Google); Daniel Marek (Google)

November 07, 2017

Google On Campus!

Come listen about how Google runs their clusters and what Borg has to do with it, how we do planet-wide atomic transactions with SQL and extreme scalability and why certain uncertainty is your friend, and also about how life at Google is and how to taste it as a software engineering intern.


Alexander Scheran (DynaTrace); Philipp Lengauer (DynaTrace)

October 24, 2017

Dynatrace - monitoring large scale production environment

Dynatrace enables full-stack monitoring for big production environments. In this talk, we will illustrate the challenges that arise when monitoring software in production and how we deal with them. We will also describe a novel approach on how to track object allocations on a per-path basis to minimize run-time overhead.


Vasilios Andrikopoulos (University of Groningen)

October 17, 2017

Large scale complex, dynamic, and collaborative systems - present and future

The maturation of service choreographies empowers the creation and operation of complex distributed software systems with collaborative and adaptive characteristics. Such systems appear in different areas of interest, e.g. pervasive systems and scientific workflows. The availability of resources on demand through cloud computing allow for scaling the infrastructure required for their instrumentation. At the same time, however, a number of challenges arise related to the cloudification of the necessary middleware and the related trade-offs between cost and performance of such systems. In this talk we discuss our effort towards addressing these challenges, as well as present a vision for a next generation of widely distributed, large scale systems which combine different computing paradigms.


Ján Veselý (Rutgers University, USA)

June 06, 2017

GPU System Calls

We explore how to directly invoke generic system calls in GPU programs. We examine how system calls should be meshed with prevailing GPGPU programming models, where thousands of threads are organized in a hierarchy of execution groups: Should a system call be invoked at the individual GPU task, or at different execution group levels? What are reasonable ordering semantics for GPU system calls across these hierarchy of execution groups? To study these questions, we implemented GENESYS – a mechanism to allow GPU programs to invoke system calls in the Linux operating system. Numerous subtle changes to Linux were necessary, as the existing kernel assumes that only CPUs invoke system calls. We analyze the performance of GENESYS using micro-benchmarks and three applications that exercise the filesystem, networking, and memory allocation subsystems of the kernel. We conclude by analyzing the suitability of all of Linux’s system calls for the GPU.


Alberto Griggio (Fondazione Bruno Kessler, Italy)

June 02, 2017

Satisfiability and Verification Modulo Non-Linear Arithmetic via Abstraction Refinement

We present a novel technique for Satisfiability Modulo the quantifier-free theory of nonlinear arithmetic with transcendental functions over the reals. The approach is based on an abstraction-refinement loop, in which the nonlinear functions are represented as uninterpreted in the abstract space, which is described in terms of the combined theory of linear arithmetic on the rationals with uninterpreted functions. Nonlinear functions are incrementally axiomatized by leveraging techniques from differential calculus, using a lemmas-on-demand approach. Besides presenting the basic solving procedure, we also discuss how to integrate it in state-of-the-art SMT based techniques for the verification of transition systems with nonlinear constraints.


Vlastimil Dort

May 30, 2017

Checker Framework

The seminar will introduce the Checker Framework developed at University of Washington. The framework provides type checking of pluggable type systems for Java. Each type system is defined in terms of a collection of Java type annotations, which can be applied to types in Java 8 code. The Framework also comes with various type systems and checkers designed to find and prevent common bugs such as null pointer dereferences, out-of-bounds array accesses or invalid format strings.


Rima Al Ali

May 16, 2017

Collective Adaptive Systems Use Cases in EU Projects


Pavel Parízek

April 25, 2017

Efficient Search for Concurrency Errors and Debugging


Vladimír Matěna

April 11, 2017

Communication in intelligent ensembles


Antti Hyvärinen (USI Lugano)

April 05, 2017

Scalable Constraint Solving

Modeling systems and reasoning about their properties in an automatic and scalable way is increasingly important in a variety of modern applications. For such an approach to be successful it is necessary to find a compromise between the expressibility of the modeling language and the efficiency of the deduction engine. The Satisfiability Modulo Theories (SMT) framework integrates a modeling language with the solving machinery, but provides little support for automatically adjusting the language to fit the needs of a particular modeling task. The proposed research answers this challenge through a natural combination of SMT theories and techniques for over-approximating and refining the model based on counter-examples that is at the same time capable of adjusting to a computing environment with a high degree of parallelism.


Antonín Steinhauser

March 14, 2017

Context-sensitive XSS

Cross-site scripting bugs are not always caused by missing sanitization of user inputs. Sometimes the inputs are sanitized, but the sanitization is incompatible with output context of the sanitized value. That can leave the application vulnerable as if no sanitization was used, but it’s impossible to discover these bugs with traditional taint tracking. We propose an extension of dynamic taint tracking for web applications that can successfully discover these context-sensitive cross-site scripting bugs.


Paolo Arcaini

March 01, 2017

MutRex: a mutation-based generator of fault detecting strings for regular expressions

Regular expressions permit to describe set of strings using a pattern-based syntax. Writing a correct regex that exactly captures the desired set of strings is difficult, also because a regex is seldom syntactically incorrect, and so it is rare to detect faults at parse time. We propose a fault-based approach for generating tests for regexes. We identify fault classes representing possible mistakes a user can make when writing a regex, and we introduce the notion of distinguishing string, i.e., a string that is able to witness a fault. We provide a tool, based on the automata representation of regexes, for generating distinguishing strings exposing the faults introduced in mutated versions of a regex under test. The basic generation process is improved by two techniques, namely monitoring and collecting. Experiments show that the approach produces compact test suites having a guaranteed fault detection capability, differently from other test generation approaches.


Jan Kofroň

February 22, 2017

Tutorial on formal methods II.

The seminar will introduce the basic concepts and algorithms used in software verification and model checking to make the subsequent specialized seminars more comprehensible for people from outside this research area.


Vojtěch Horký

January 10, 2017

Tutorial on performance evaluation: comparing alternatives

The seminar will introduce the basic concepts of statistical evaluation of computer performance data. The focus will be on statistical methods that are useful for evaluation whether two data sets differ (e.g. to detect performance regressions). Practical behaviour of the statistical methods on real data will be reported.


Jakub Daniel

December 21, 2016

Property-directed Symbolic Model Checking of Safety Properties


Steffen Becker (TU Chemnitz)

December 14, 2016

Atos training course

An ever increasing number of developers are work-ing in the software industry for some time after completing their studies or equivalent education. Their knowledge on recent software engineering topics is often limited and needs to be kept up-to-date in regularly training courses. One of the topic areas often not known to those developers is that of software architectures. It is an abstract topic covering component selection and composition, architecture documentation and evaluation as well as the skills and tasks needed by architects. Several books exist covering all aspects of software architecture and their number is still increasing. Based on these books, some proposals for architecture courses, in particular at universities, have been published. Using the available background material and our own experience, we have designed and conducted a training course on software architecture for senior level developers from Atos, one of Europe’s largest software development companies. While teaching our course we learned several lessons, in particular that the approach of using physical bricks to represent components is a suitable way to approach the topic for educating senior staff.


Rima Al Ali

December 13, 2016

Time Series Analysis to Architecture Modes in Smart Cyber Physical Systems


Vlastimil Dort

December 06, 2016

Abstract Interpretation of Programs with Strings


Martin Blicha

November 22, 2016

Partial Variable Assignment Interpolants

Craig interpolants are widely used in program verification as a means of abstraction. Computed interpolants are often used again in later steps in verification algorithms as part of SAT/SMT queries. Since querying solver is an expensive operation, it is desirable for the interpolants to be as small as possible. A variable assignment focuses computed interpolants by restricting the set of clauses taken into account during interpolation. A framework of Labeled Partial Assignment Interpolation Systems has been proposed for computation of such focused interpolants. We show that if a general input is considered (in contrast to input expected in CNF), the framework can be improved to further reduce the size of the computed interpolants.


Jiří Vinárek

November 16, 2016

Overview of the RoboCup Rescue Simulation challenge

The Robocup Rescue Simulation Platform is a comprehensive simulation environment for research in disaster response management. The talk presents an overview of the platform, challenges related to coordination of a multi-agent system in the simulation and common approaches coping with the complexity of the environment.


Jan Tattermusch (Google)

November 15, 2016

gRPC - A solution for RPCs by Google


Petr Tůma

November 09, 2016

Tutorial on performance evaluation experiments in managed environments


Jan Kofroň

November 01, 2016

Tutorial on formal methods I.

The seminar will introduce the basic concepts and algorithms used in software verification and model checking to make the subsequent specialized seminars more comprehensible for people from outside this research area.


Filip Krijt

October 25, 2016

Automated ensemble formation based on high-level DSL description and domain data

Smart cyber-physical systems place great emphasis on autonomous component operation as well as opportunistic cooperation, and ensemble-based components models such as DEECo allow us to implement both without violating core architectural principles. However, while the current implementation of DEECo theoretically supports ensembles of all forms, some more complicated cases must be implemented manually by having a component decide the structure of the system, thus polluting the business logic with coordination code. To address this, we have introduced ensemble definition language (EDL) and enriched the ensemble semantics with more powerful coordination constructs. By allowing developers to directly describe the coordination constraints and goals, such a language can then be used for partially automating the sCPS software process, thus both decreasing the likelihood of human error and increasing the confidence of the architect in the code. This seminar presents an overview of the current features of the EDL and its runtime realization, implemented via the Java EMF tools, XText, and the Z3 SMT solver.


Marco Eilers (ETH Zürich)

October 19, 2016

Nagini: Verifying Python Programs in Viper

Dynamic languages like Python and JavaScript have gained popularity because of their expressiveness and ease of use. They are increasingly being used even for critical applications with high correctness demands. However, the state of the art in static analysis and program verification provides little support for reasoning about such programs. In this talk, we present Nagini, a verifier for Python. Nagini takes Python programs that include statically-checkable type annotations as well as contracts, and encodes them into the Viper verification infrastructure. We will explain some highlights of this encoding and show how to write specifications for programs that make use of object-orientation and polymorphism. We also outline some advanced verification techniques for liveness properties and Input/Output behavior.