Event Category: Colloquium

Axiomatization of branching bisimulation for distributions has been established in the setting of a process language with nondeterministic and probabilistic choice in earlier work. Key ingredient to the proof of completeness of the proposed theory is the notion of stability of processes and the property that every distribution can evolve, within the same equivalence class …continue reading

In feature-oriented software development, software product lines are defined as families of systems where features encapsulate incremental or optional behaviors. There are mainly two different approaches for specifying feature-oriented systems: either annotative of compositional, i.e., either guarding code by presence conditions over features or specifying components for each feature along with a composition operation. Both …continue reading

Besides the official LEGO sets there are many fan-created designs online. To build these custom designs you need to buy individual parts online. Concentrated on two larger platforms there are thousands of stores offering parts. An interesting optimisation problem arises: which distribution of parts over the stores is the cheapest, also considering shipping costs? In …continue reading

Language workbenches have been developed to ease the implementation of Domain Specific Languages (DSLs), which are used often in industry for better productivity and communication among engineers. However, only very little literature exists that evaluates the use of a language workbench for an industrial context. In a work in progress journal paper we do exactly …continue reading

In a previous colloquium, we presented a new and efficient readers-writer lock with no resource contention between readers, called the Busy-Forbidden Protocol. For its verification, specifications of its implementation and its less complex external behavior are provided. However, we are unable to prove the equivalence of these models for more than 7 concurrent threads using …continue reading

The toolset heavily relies on boolean equation systems, which are the workhorse to solve modal formulas. Boolean equation systems only permit truth values as solutions for variables. It would be nice to also extract quantitative information using modal formulas, such as probabilities, durations, or yields. For this purpose it would be nice to have real …continue reading