ANC Seminar: Danny Tarlow, Microsoft Research Chair: Iain Murray
Learning to Decipher the Heap for Program Verification
What 


When 
Sep 08, 2015 from 11:00 AM to 12:00 PM 
Where  IF 4.31/4.33 
Add event to calendar 
vCal iCal 
An open problem in program verification is to verify properties of computer programs that manipulate memory on the heap. A key challenge is to find formal descriptions of the data structures that are instantiated at different program points (heap invariants), which are used as input to a proof procedure that verifies the program. Standard approaches to the problem are to severely restrict the space of data structures that can be recognized (e.g., just lists), or to use search guided by handspecified heuristics.
In this talk, I'll give an overview of our work on phrasing this invariant prediction problem as a machine learning problem, where we execute the programs and then learn to map the state of heap memory (represented as a labelled directed graph) to a logical description of the instantiated data structures (in a logic known as separation logic). I'll describe two approaches to the problem: one using a treestructured model of the logical description's parse tree, and one using graphstructured neural networks. I'll present preliminary empirical results showing this to be a promising new direction.
http://www.cs.toronto.edu/~dtarlow/