Seminar

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

---

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

---

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.

---

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.

---

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.

---

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!

---

---

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.

---

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.

---

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.

---

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.

---

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.

---

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.

---

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.

---

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.

---

---

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.

---

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.

---

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.

---

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.

---

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.

---

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.

---

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.

---

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.

---

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).

---

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.

---

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.

---

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.

---

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.

---

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.

---

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.

---

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

---

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.

---

---

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?

---

---

---

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.

---

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.

---

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.

---

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.

---

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.

---

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.

---

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.

---

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.

---

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.

---

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.

---

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.

---

---

---

---

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.

---

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.

---

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.

---

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.

---

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.

---