Personal tools
You are here: Home Events ANC Seminar: Danny Tarlow, Microsoft Research Chair: Iain Murray

ANC Seminar: Danny Tarlow, Microsoft Research Chair: Iain Murray

— filed under:

Learning to Decipher the Heap for Program Verification

What
  • ANC/DTC Seminar
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 hand-specified 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 tree-structured model of the logical description's parse tree, and one using graph-structured neural networks. I'll present preliminary empirical results showing this to be a promising new direction.

 

 

http://www.cs.toronto.edu/~dtarlow/