Hiding global invariants by local reasoning in region logic

  • Dave Naumann | Stevens Institute of Technology, Hoboken, NJ, USA

Higher order frame rules in separation logic provide a way to understand disciplines such as ownership for information hiding in object based programs.
Recent work of Banerjee, Naumann, and Rosenberg uses explicit regions to express, in classical first-order assertions, the read-footprints of predicates and write-footprints of commands, supporting an ordinary frame rule. On this basis, I give a second order frame rule, show its admissibility, and describe its use in encoding disciplines like ownership.

Speaker Details

Dave Naumann is on the faculty of Computer Science at Stevens Institute of Technology. His current research focus is on how to exploit established verification technologies for specification and modular static analysis of security properties. His current musical focus is Rebetika.

Watch Next