Keynote talk IIP: Proving (and revisiting) what programs do not

Summary form only given. In 2007, I had the honor of an invited presentation at MEMOCODE, where I discussed the frame problem: how to establish that programs do not modify certain properties. The problem is particularly challenging in the case of object-oriented programs involving complex pointer (reference) data structures. Seven years later, it is still largely an open problem, although significant progress has occurred. After realizing that a satisfactory solution requires addressing another difficult problem, alias analysis, I have devoted much of my work to program analysis techniques that tackle both aliasing and framing. Taking advantage of the kind invitation to present again at MEMOCODE, I will describe the current state of this work and how its results are embodied in program analysis tools that provide automatic means - not requiring program annotations - to ascertain fundamental properties of programs.