7 Março 2017, 23:13 - Maria de Lurdes Piado Farrusco
Title: Automatic Verification for Fine-grained Concurrency
Speaker: Pedro da Rocha Pinto, Imperial College London, UK
Date and time: Monday, March 13, 4pm
Location: CSE meeting room (Informática II - Alameda), videocast to DSI room in Tagus.
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.Bio
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.