We are interested in dynamic heap management which provides the performance and predictability of explicit memory management with the ease of use of implicit memory management. To gain new insights we designed a new heap management model which may provide an interesting target for program analysis and code generation of explicit memory management code.

In our new heap management model, called short-term memory, objects on the heap expire after a finite amount of time, which makes deallocation unnecessary. Expiration of longer-needed objects may be extended by refreshing.

The generation of refresh calls seems more feasible than the generation of free calls for several reasons:

• In short-term memory it is valid to refresh an object multiple times, which allows to conservatively add refresh calls for all objects which are potentially needed, even if no refreshing would be necessary.
• Only needed objects require refreshing. Needed objects are always reachable, independent of the code location. This may allow more flexible positioning of memory management code for code generation.

Our current implementation [SBG10c] uses logical clocks controlled by explicit tick calls. The positioning of tick calls influences the memory consumption, since with faster time advance objects may expire earlier. In first experiments we added tick and refresh calls manually. We ported applications written in C, Java, and Go to use short-term memory with a single clock and got competitive performance in time and space. In a next step we will place refresh and tick calls automatically, and we will employ multiple clocks to allow better code generation and program analysis, and to further improve runtime behavior.

Transactional memory (TM) has shown potential to simplify the task of writing concurrent programs. Recent studies have shown that the conflict detection mechanisms for TM do not allow the performance of TM to scale to that of fine-grained locking in concurrent data structures. This has led researchers to relax the conflict detection for transactions, using mechanisms like early release and elastic transactions.

We formalize the notion of relaxed transactional access models and their desired properties. We introduce a new transactional access model, peek-quake model, that allows two new commands, peeks (a lighter form of read) - and its dual quakes (a heavier form of write) - for finer conflict detection in STM. In our augmented model, a normal read conflicts with every write, while a peek conflicts only with quakes. We compare the peek-quake access model to existing access models in our formalism. We use the peek-quake access model to implement concurrent data structures like linked list based sets and red-black trees. We extend the TL2 implementation with support for peek and quake commands. We evaluate the performance of the peek-quake based TL2 on the linked list based set and red-black tree (microbenchmarks) and STAMP benchmarks. Compared to TL2, we observe performance gains of upto 2x for the microbenchmarks, and 1.2x for the genome benchmark.

We present LLBMC, a tool for bounded model checking of C programs. LLBMC uses the LLVM compiler framework to translate C programs into LLVM's intermediate representation. The resulting code is then converted into our own logical intermediate representation and simplified using rewrite rules. The simplified formula is finally passed to an SMT-solver. In contrast to existing tools, LLBMC uses a bit-precise memory model. It thus can handle, e.g., memory-based re-interpret casts, which frequently occur in system level programs.

The semantics of a concurrent object is determined by a correctness condition (e.g. linearizability) and a sequential specification (e.g. FIFO). An implementation of a concurrent object may incur high synchronization overhead for realizing the semantics and thus limit scalability. A relaxed version of a given correctness condition and sequential specification may allow us to gain scalability at the expense of deviating from the original semantics (e.g. linearizable FIFO). We study the trade-off between scalability and semantical deviation based on concurrent FIFO queues and present concurrent object components that allow us to control that trade-off and provide scalability even under high contention scenarios [PODC 2011 Brief Announcement].

Computer science has seen a long push from imperative to declarative programming, which has failed miserably. The idea that the programmer should state *what* should be computed instead of *how* has lead to languages like Prolog, Lisp, and Caml, which have never become mainstream. We argue that computations are much easier programmed imperatively, but that the same does not hold for concurrency. In concurrency statements of correctness may be as simple as "no race conditions", or, "the functionality of the program is the same whether it runs on one or two processors." Thus, we need a programming paradigm that combines the strengths of imperative languages where data is concerned with those of declarative programming for concurrency. We argue that this line of research deserves more attention and look at some initial ideas to make it real.

Software testing is an expensive and time consuming process, often involving the manual creation of comprehensive test suites. However, current testing methodologies do not take full advantage of these tests. We introduce a technique for augmenting existing test cases with no additional human effort, via a lightweight symbolic execution mechanism. Our prototype implementation found a previously unknown bug in the cut GNU Coreutils program, which goes undetected by the regression suite or extensive symbolic execution alone.

We describe an approach to model-based testing where a test suite is generated from a model and automatically concretized to drive an implementation. Motivated by an industrial project involving DO-178B compliant avionics software, where the models are UML activity diagrams and the implementation is ANSI C, we developed a seamless testing environment based on our test specification language FQL. We demonstrate how to apply FQL to activity diagrams in such a way that FQL test specifications easily translate from UML to C code. Our approach does not require any additional glue or auxiliary code but is fully automatic except for straightforward source code annotations that link source and model. In this way, we can check for modeled but unimplemented behavior and vice versa, and we can also evaluate the degree of abstraction between model and implementation.