We present an effect based static analysis to calculate upper and lower bounds on the memory resource consumption in a transactional calculus. The calculus is a concurrent variant of Featherweight Java extended by transactional ...

The GI Working Group“Programming Languages and Computing Concepts” arranges since 1984 each spring a workshop in the the “Physikzentrum Bad Honnef” (a convention centre of the German Physical Society). The meeting serves ...

This report extends our behavioral type and effect system for detecting dealocks in [8] by polymorphism and formalizing type inference (wrt. the lock types. Our inference is defined for a simple concurrent, first-order ...

Railway systems designs deal with complex and large-scale, safety-critical infrastructures, where formal methods play an important role, especially in verifying the safety of so-called interlockings through model checking. ...

Hybrid systems are systems that exhibit both discrete and continuous behavior. Reachability, the question of whether a system in one state can reach some other state, is undecidable for hybrid systems in general. The ...

Deadlocks are a common error in programs with lock-based concurrency and are hard to avoid or even to detect. One way for deadlock prevention is to statically analyze the program code to spot sources of potential deadlocks. ...

In this paper, we formalize an operational semantics of a weak memory model similar to the one in Go, concentrating on buffered writes, i.e., ignoring the possibility of buffered reads.

Feil nr (409) på tittelbladet. Skal være Research report nr 406.

A multitude of weak memory models exists supporting various types of relaxations and different synchronization primitives. On one hand, they must be lax enough to allow for hardware and compiler optimizations; on the other, ...

The GI Working Group“Programming Languages and Computing Concepts” arranges since 1984 each spring a workshop in the the “Physikzentrum Bad Honnef” (a convention centre of the German Physical Society). The meeting serves ...