Verifying weak memory concurrent data structure implementations

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...

Finite Abstractions of Network Calculus Elements for Formal Verification of Network Bounds

This thesis presents a method to semi-automate the reasoning about network bounds, namely the backlog and delay. Network Calculus offers a rich theory for modeling network elements. Using the modeling techniques of network calculus, network elements are represented by discrete-time systems whose dynamics are linear in min-plus algebra. From the...

Model checking GOAL agents

This thesis presents a novel approach to model checking of agent programs written in an agent programming language. The language we consider is GOAL. The novelty of the approach is that we implement model checking algorithms from scratch on top of the standard language interpreter. In contrast, in the literature on agent program verification,...