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-05-30 14:00 in S9: Checker Framework

Vlastimil Dort

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.

2017-06-02 09:00 in S5: Satisfiability and Verification Modulo Non-Linear Arithmetic via Abstraction Refinement

Alberto Griggio (Fondazione Bruno Kessler, Italy)

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.

2017-06-06 10:00 in S5: GPU System Calls

Ján Veselý (Rutgers University, USA)

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.

Past Seminars (one year back)

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

Date Title Speaker(s) Details
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
2016-11-16 Overview of the RoboCup Rescue Simulation challenge Jiří Vinárek
2016-11-15 gRPC - A solution for RPCs by Google Jan Tattermusch
2016-11-09 Tutorial on performance evaluation experiments in managed environments Petr Tůma
2016-11-01 Tutorial on formal methods I. Jan Kofroň
2016-10-25 Automated ensemble formation based on high-level DSL description and domain data Filip Krijt
2016-10-19 Nagini: Verifying Python Programs in Viper Marco Eilers
(ETH Zürich)
2016-10-19 Viper - A Verification Infrastructure for Permission-based Reasoning Malte Schwerhoff
(ETH Zürich)
2016-10-05 News in Java Petr Hnětynka
2016-06-28 String Analysis for Code Contracts Vlastimil Dort
2016-06-22 Narrowing the Uncertainty Gap between Software Models and Performance Results Catia Trubiani
(GSSI, Italy)
2016-06-14 Self-Adaptive Software Systems Danny Weyns
(Katholieke Universiteit Leuven and Linnaeus University Sweden)
2016-06-01 Processes of Software Development and Maintenance Václav Rajlich
(Wayne State University, US)
2016-05-31 Autonomous Agent Behaviour Modelled in PRISM Ruth Hoffmann
(University of Glasgow, UK)
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