This scientific meeting is a PhD meeting with 5 talks delivered by PhD students.
Program
Kasper Dokter (Formal Methods)
Scheduling of Parallel Applications
Abstract: Most parallel applications leave the scheduling problem of their constituent processes to a general purpose scheduler, such as an operating system scheduler. Generally, constituent processes of a parallel application interact. For example, one process interacts with another by using its produced data. These interactions of processes introduce dependencies amongst them. However, general purpose schedulers are unaware of these dependencies, which can have negative impact the performance of the application. The work presented in this talk aims to overcome this deficiency by synthesizing interaction-aware schedulers for parallel applications.
Bart Kamphorst (Stochastics)
Achievable Performance of Blind Scheduling Policies
Abstract: We consider a single scheduler that is faced with the problem of minimizing the average flow time of tasks. Since the optimal scheduling discipline for this problem is known (SRPT), the scheduler only needs to know the duration of each task in order to easily optimize his system. Unfortunately, the scheduler does not know the durations, nor how to estimate them. Moreover, he has no idea how this lack of information affects his performance.
In this short talk I will illustrate how combined techniques from competitive analysis and applied probability have been able to give asymptotic bounds on the performance gap. More specifically, if the scheduler applies the RMLF algorithm, the performance gap scales as a logarithmic function of the work intensity as this intensity tends to one (heavy traffic).
Teresa Piovesan (Networks & Optimization)
Communication using quantum entanglement: benefits and limitations
Abstract: Everyday activities such as browsing the internet or telephone communication rely on a mathematical framework that studies the amount of data that can be transmitted through a classical communication channel. Can quantum entanglement be used to improve the performance of this classical task? We will discuss some positive and negative results, focusing in particular on the zero-error scenario.
Casper Rutjes (Multiscale Dynamics)
The origin of lightning
Abstract: Measurements of electric fields in thunderclouds show values well below the threshold for electric breakdown. Furthermore, free electrons in thunderclouds, needed to start the initial discharge, are hard to find. We have shown that three ingredients together are able to start electric breakdown in these conditions: a thundercloud electric field, a hydrometeor and an energetic cosmic particle. These initial breakdowns could lead to observed narrow bipolar events and potentially grow to a full lighting stroke.
Jouke Stoel (Software Analysis and Transformation)
Solving the Bank, on the application of formal specifications and SMT solving inside a bank
Abstract: Many large organizations like banks suffer from the ever growing complexity of their systems. As requirements and technological platforms change, the IT landscape becomes harder and harder to understand and maintain. A large contributing factor to this problem, is that the actual domain knowledge is implicit, incomplete, or out of date. The use of informal documents (Word files or Excel sheets) makes it hard to relate requirements to the actual implementation in the software. How to evolve the software in the face of change, becomes tacit knowledge of the people in the organization. As a result, the ability to predict and control the correctness, cost-of-ownership, performance and reliability is compromised.
In collaboration with a large consumer bank we developed the formal specification language Rebel. Rebel specifications can be simulated and checked by translating the specifications to SMT formulas which can be interpreted by an existing SMT solvers like Microsofts Z3. These specifications can then be used to automatically check existing systems within the bank and, ultimately, to generate applications that are correct-by-construction.
