Caper: Automatic Verification with Concurrent Abstract Predicates

Thomas Dinsdale-Young

Recent developments have been made in program logics based on separation logic. These logics emphasise a modular approach to prove functional correctness for fine-grained concurrent programs, but have no automation support. I present Caper, a prototype tool for automated reasoning in such a logic, the logic of Concurrent Abstract Predicates (CAP). Caper is based on symbolic execution, integrating reasoning about interference on shared data and about ghost resources that are used to mediate this interference. This enables Caper to verify functional correctness of fine-grained concurrent algorithms.