NECEC 2017 has ended
View analytic
Wednesday, November 15 • 10:20 - 10:40
Concurrent Software Verification with Explicit Transfer of Permission

Sign up or log in to save this to your schedule and see who's attending!

Concurrent software is difficult to reason about and impossible to verify by testing. Yet much software written today is concurrent. We therefore need practical mechanisms to automatically verify concurrent software. I propose a way of annotating concurrent programs based on fractional permissions, dynamic frames, and explicit transfer of permissions. An annotated program may be automatically verified by translating to a sequential intermediate verification language such as the Boogie IVL and then verifying a set of sequential fragments.

Wednesday November 15, 2017 10:20 - 10:40
Conception Bay South 180 Portugal Cove Road, St. John's, NL, Canada

Attendees (2)