D3S Seminar – Department Meeting

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 S9 and Wednesdays at 9: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

2017-11-28 14:00 in S9: An Ensemble-based Approach For Scalable QoS in Highly Dynamic CPS

Vladimír Matěna

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.

2017-11-29 09:00 in S5: Sampling Invariants from Frequency Distributions

Grigory Fedyukovich (University of Washington)

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.

2017-12-06 09:00 in S5: topic to be announced

Dominik Škoda

abstract to be announced

2017-12-13 09:00 in S5: topic to be announced

Jiří Vinárek

abstract to be announced

2017-12-20 09:00 in S5: topic to be announced

Rima Al Ali

abstract to be announced

2018-01-09 14:00 in S9: topic to be announced

Petr Kubát

abstract to be announced

2018-01-10 09:00 in S5: topic to be announced

Vlastimil Dort

abstract to be announced

Past Seminars (one year back)

You can also view a verbose list of all past seminars.

Date Title Speaker(s) Details
2017-11-14 Automated Repairing of Variability Models Paolo Arcaini
2017-11-07 Google On Campus! Ondřej Šerý
(Google)Daniel Marek
2017-10-24 Dynatrace - monitoring large scale production environment Alexander Scheran
(DynaTrace)Philipp Lengauer
2017-10-17 Large scale complex, dynamic, and collaborative systems - present and future Vasilios Andrikopoulos
(University of Groningen)
2017-06-06 GPU System Calls Ján Veselý
(Rutgers University, USA)
2017-06-02 Satisfiability and Verification Modulo Non-Linear Arithmetic via Abstraction Refinement Alberto Griggio
(Fondazione Bruno Kessler, Italy)
2017-05-30 Checker Framework Vlastimil Dort
2017-05-16 Collective Adaptive Systems Use Cases in EU Projects Rima Al Ali
2017-04-25 Efficient Search for Concurrency Errors and Debugging Pavel Parízek
2017-04-11 Communication in intelligent ensembles Vladimír Matěna
2017-04-05 Scalable Constraint Solving Antti Hyvärinen
(USI Lugano)
2017-03-14 Context-sensitive XSS Antonín Steinhauser
2017-03-01 MutRex: a mutation-based generator of fault detecting strings for regular expressions Paolo Arcaini
2017-02-22 Tutorial on formal methods II. Jan Kofroň
2017-01-10 Tutorial on performance evaluation: comparing alternatives Vojtěch Horký
2016-12-21 Property-directed Symbolic Model Checking of Safety Properties Jakub Daniel
2016-12-14 Atos training course Steffen Becker
(TU Chemnitz)
2016-12-13 Time Series Analysis to Architecture Modes in Smart Cyber Physical Systems Rima Al Ali
2016-12-06 Abstract Interpretation of Programs with Strings Vlastimil Dort
2016-11-22 Partial Variable Assignment Interpolants Martin Blicha
Logo of Faculty of Mathematics and Physics
  • Phone: +420 951 554 267, +420 951 554 236
  • Email: info<at-sign>d3s.mff.cuni.cz
  • How to find us?
Modified on 2016-05-04