Tool Support for Separation Logic

Seminar

Separation Logic is a powerful formalism for reasoning about programs that manipulate memory, particularly in systems that involve shared mutable data structures such as pointers and heap allocations. It enables modular verification by partitioning memory into disjoint regions, making it easier to reason about different parts of memory in isolation. This modularity is particularly useful for verifying concurrent programs, where multiple threads access shared memory.

In recent years, several tools have been developed to support semi-automated verification using Separation Logic. Tools such as VeriFast, VerCors, and Viper are well-known examples, but there are many other tools available that implement variations of Separation Logic. Each tool provides unique features, such as proof assistance, symbolic execution, proof automation, and integration with modern programming languages.

Goal

In this seminar, you will explore the state of the art in tool support for Separation Logic by comparing the capabilities of various tools and evaluating their effectiveness in verifying real-world programs. You will select a set of example programs and verify them using the chosen tools, identifying their strengths and weaknesses regarding memory safety, concurrency, and other verification challenges.

Additionally, you will investigate whether non-deductive verification tools—such as bounded model checking or other approaches—use a notion of separation, and how these compare to deductive tools in handling separation concepts.

Starting Points