PhD student on the subject of Verification of Mainstream Java Libraries

The overall objective of this PhD position is the development and application of formal methods to actual software. Of particular interest are the mainstream libraries of the popular programming language Java. These libraries are widely used and therefore their correctness is of the utmost importance. This research builds on and extends the successful verification by means of the interactive theorem prover KeY of executable Java versions of Counting sort and Radix sort. A recent attempt to verify the Java implementation of the TimSort hybrid sorting algorithm as provided by the Java Collections Framework (and which is designed to perform well on real world data) revealed a fundamental error which for certain inputs crashed the software. In close collaboration with the Software Engineering group of TU Darmstadt, we succeeded in the verification of the corrected software. Motivated by this success our overall goal is the systematic verification of the Java Collections Framework. As a PhD you will contribute to the realization of this ambitious goal by a further development of the interactive theorem prover KeY, which is required to master the complexity of correctness proofs, and the application of the interactive theorem prover KeY to the Java Collections Framework.

Postdoc in the research project "Approximation Algorithms, Quantum Information and Semidefinite Optimization"

The research project “Approximation algorithms, quantum information and semidefinite optimization” aims to explore the limits of efficient computation within classical and quantum computing, using semidefinite optimization as a main unifying tool. The position involves research into the mathematical and computer science aspects of approximation algorithms for discrete optimization, quantum entanglement in communication, and complexity of fundamental problems in classical and quantum computing. More information about the project can be found at this website.

Project Researcher / Postdoc (1 year) on the subject of Blockchains, Dynamic Contracts and Autonomous Negotiation for Smart Grids

Energy systems are currently in a revolutionary transition, due to the increasing inclusion of sustainable energy sources. Whereas in the past, energy supply was determined by demand and was supplied centrally, in the future, demand and increasingly decentralized supply will need to respond to each other. Their balancing requires a combination of adjusting conventional generation, exploiting efficient storage technologies and implementing demand response with corresponding incentives thereof. Balancing activities may take place on multiple scales, from the individual household to the European or even an envisioned global grid. The vacant position contributes to the research, development and experimentation to tackle applied scientific research questions within the EIT Digital project ‘Distributed Ledger Services for Online Contract Settlement (DLS OCS)’. The primary driver is increasing system efficiency by a fair attribution of energy planning and plan-deviation costs between multiple stakeholders. The aims of DLS-OCS are to extend the state of the art in (1) Contract definitions, specifically for trading electric flexibility (demand response), (2) Negotiation strategies, specifying how parameters of the contracts are agreed upon by autonomous agents, (3) Use-case scenarios, how a blockchain-based solution can provide services in the energy context. The research shall draw on tools and techniques from sequential multi-agent decision-making under uncertainty, (evolutionary) game theory and market mechanism design. The project is a European collaboration, and the research is closely related to other research activities within the group. The applicant will take responsibility for the implementation of algorithms and contracts for planning and intelligent local control in face of uncertainty, and will closely collaborate with other project team members. Overall, the work is aimed at developing reusable software algorithms, simulation and control modules that can be employed in scientific experiments related to the research in the group

Postdoc on the subject of Network Games with Combinatorial Structures

The goal of this project is to study the computation and inefficiency of equilibria in strategic games on networks. One key aspect is to identify combinatorial structures that allow for the efficient computation of equilibria with provable inefficiency guarantees. Another key aspect is to investigate the potential of exploiting combinatorial structures to develop coordination mechanisms that reduce the inefficiency caused by selfish behavior.

Postdoc / Postdoctoral Researcher on the subject of the computer-science aspects of quantum computing and quantum information theory

This position involves research into the computer-science aspects of quantum computing and quantum information theory, in close cooperation with Prof. Ronald de Wolf. Specifically, the project will focus on the development of new quantum algorithms and the analysis of their complexity, development of new quantum communication protocols and the role entanglement plays in such protocols, and applications of quantum techniques to problems in classical computer science and mathematics.