In this thesis, we design a program logic for reasoning about data protection properties. Our logic features an assertion language based on first-order temporal logic, which we use to encode both past and future properties. We codify a notion of obligations for expressing future assertions that must become true during program execution. We apply our program logic to express data protection properties and prove them for a realistic program.
Show all metadata 