Verifying fine-grained concurrent algorithms with VeriFast

Bart Jacobs

I will introduce my VeriFast program verifier prototype, and explain how I used it to verify Harris et al.'s multiple-compare-and-swap algorithm, a challenging lock-free data structure. The tool accepts single-threaded and multithreaded programs written in a subset of C or Java and annotated with preconditions, postconditions, loop invariants, inductive datatypes, recursive pure functions over these datatypes, recursive separation logic predicates, and recursive lemma routines that serve as inductive proofs. I will demonstrate the interactive annotation authoring experience using the VeriFast IDE.