Name: Cong Quy Trinh, PhD student in Uppsala University, Sweden

Topic: Formal Verification of Skiplist Algorithms

Abstract: We consider the problem of automatically verifying correctness of
concurrent algorithms with an unbounded number of threads that access a
shared heap. In particular we look at algorithms that manipulate
skiplist-like data structures that have not been verified formally yet.
Skiplists are challenging and they have escaped attempts of automated formal
verification. For such algorithms, we propose a methodology for generating
and checking program invariants. As illustrative, we manually apply
the technique
to a concurrent skiplist algorithm from the literature