From formal hardware models to programming language implementations concurrency is everywhere. While there has been a lot of work done on verifying concurrent systems a large part of it is focused on SC. In practice, it is more common to encounter weak memory models for which the techniques developed for SC do not work. There exists previous research on verifying weak memory concurrent programs, however, this work is often limited in scope and is often difficult to understand and apply to a broader context. This thesis gives a general approach for calculating higher-level relations between function calls in a weak memory context that work for weak memory concurrent mutex, stack, and queue data structures. These relations allow us to abstract away implementation details for easier reasoning about program behaviour. These function-level relations and data structure models defined using them are implemented in a stateless model checker and used to verify several existing mutex, stack, and queue implementations.

Finding good viewpoints for catoptric anamorphoses by hand is hard. However, it should be possible to find the optimal viewpoint using just the specifications of the mirror. This problem is solved by first generating a set of candidate viewpoints using the specifications of the mirror. Then all candidates are ranked based on metrics like visible surface area. The optimal is then easily found.