Scientific publications

Maintaining large, multi-language code bases is challenging because of their size and complexity. Hence, tool support is desirable. Unfortunately, off-the-shelf tools fall short by aiming for genericity instead of exploiting characteristics of the specific code bases and maintenance tasks. Our objective is to support software maintenance by facilitating the development of custom tools for static code analysis.

Many real-world problems such as internet routing are actually graph problems. To develop efficient solutions to such problems, more and more parallel graph algorithms are proposed. This paper discusses the mechanized verification of a commonly used parallel graph algorithm, namely the Bellman–Ford algorithm, which provides an inherently parallel solution to the Single-Source Shortest Path problem.

At Philips IGT, we develop and produce interventional X-ray systems. For a controller in these systems, we have an approximately five years old domain specific language. Like general programming languages, domains specific languages also evolve. These languages co-evolve together with their domain. The language used at IGT was initially created for one system instance.

The rapid advancement of communication technology realized the dream of interconnected systems. In addition to enabling scalability and flexibility of solutions, this paradigm created new system design challenges. One such challenge is to holistically address security and privacy concerns of solutions early in design while respecting the system of systems context.

Gobra is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subtyping and lightweight concurrency through go routines with message-passing communication. This combination of features poses interestingchallenges for static verification, most prominently the combination of amutable heap and advanced concurrency primitives.

To increase energy efficiency of receiver-dominated nodes in IoT networks, we introduce Receiver-Sensitivity Control (RSC). RSC enables a trade-off between communication range and reception efforts. This trade-off is achieved through multiple receiver-sensitivity levels that can be adjusted at run time.

Vehicle platooning has gained attention for its potential to increase road capacity and safety, and higher fuel efficiency. Platoon controls are implemented over Vehicle-to-Vehicle (V2V) wireless communication, in-vehicle networks and Electronic Control Units (ECUs). V2V communication has a low message rate imposed by the V2V standard compared to the rate of modern in-vehicle networks and ECUs.

An elevator is used as a simple system to model a few physical aspects. We will show simple kinematic models and we will consider energy consumption. These low level models are used to understand (physical) design considerations. Elsewhere we discuss higher level models, such as use cases and throughput, which complement these low level models.