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

Pedro da Rocha Pinto completed his PhD at the Department of Computing at Imperial College London, where he has developed logics for program verification, especially for fine-grained concurrency. He now works on tools to mechanise concurrency verification as a PostDoc under Philippa Gardner at Imperial College London.