This talk will be on the area of runtime systems, focusing on the proto-runtime approach to modularizing runtime systems for parallel languages. I will show how any parallel runtime can be modularized into three modules. The first is a machine-specific module that exports an abstraction of the hardware. The other …
read moreModal mu-calculi for Probabilistic Labeled Transition Systems
I will use this talk as an opportunity to introduce my scientific work to the members of the Formal Methods group. I will present the research I have done during my PhD on the semantic foundations of "probabilistic" modal mu-calculi. This is mostly based on Game Theory, but I will …
read moreA Matter of Priority
(joint work with Christel Baier, Sascha Klüppelholz, and Joachim Klein)
Priority designates an alternative among a set of possible actions of an actor as its preferred choice. In a concurrent system that involves many independent actors, the individual actors may not have compatible priorities. Such incompatible priorities make it non-trivial …
read moreWeak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks - part 2
We present a completeness proof of the inductive assertion method for object-oriented programs extended with auxiliary variables. The class of programs considered are assumed to compute over structures which include the standard interpretation of Presburger arithmetic. Further, the assertion language is first-order, i.e., quantification only ranges over basic types …
read moreType Inference for Linear Algebra with Units of Measurement
Refining types of numerical data with units of measurement has the potential to increase safety of programming languages but is restricted to homogeneous units when checked statically with parametric polymorphism. We lift units to vectors and show how type inference of linear algebra expressions can statically determine safety for data …
read moreWeak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks - part 1
We present a completeness proof of the inductive assertion method for object-oriented programs extended with auxiliary variables. The class of programs considered are assumed to compute over structures which include the standard interpretation of Presburger arithmetic. Further, the assertion language is first-order, i.e., quantification only ranges over basic types …
read moreA process-theoretic approach to supervisory coordination
A supervisory controller controls and coordinates the behavior of different components of a complex machine by observing their discrete behaviour. Supervisory control theory studies automated synthesis of controller models, known as supervisors, based on formal models of the machine components and a formalization of the requirements. Subsequently, code generation can …
read moreOn the specification of operations on the rational behaviour of systems
Abstract: Structural operational semantics can be studied at the general level of distributive laws of syntax over behaviour. This yields specification formats for well-behaved algebraic operations on final coalgebras, which are a domain for the behaviour of all systems of a given type functor. We introduce a format for …
read moreTowards Dynamic Adaptation of the Differential Majority-Rule Solution of the Double Bridge Problem
In the double-bridge problem, a population of ants seeks to discover the shortest path from to nest to two alternative places with food. For swarmonoids, a collective of small robots which coorperate to achieve a common goal, a solution using the so-called majority rule for the double-bridge problem was recently …
read moreA Constraint-based Method to Compute Semantics of Channel-based Coordination Models
Reo is an exogenous channel-based coordination language that acts as "glue code" to tie together software components and services. The building blocks of Reo models are connectors that impose constraints on the data-flow in component or service-based architectures in terms of data synchronization, buffering, mutual exclusion, etc. Several semantic models …
read more