@TechReport{	  it:2009-018,
  author	= {Parosh Aziz Abdulla and Muhsin Atto and Jonathan Cederberg
		  and Ran Ji},
  title		= {Automated Analysis of Data-Dependent Programs with Dynamic
		  Memory},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Division of Computer Systems},
  year		= {2009},
  number	= {2009-018},
  month		= jun,
  abstract	= {We present a new approach for automatic verification of
		  data-dependent programs manipulating dynamic heaps. A heap
		  is encoded by a graph where the nodes represent the cells,
		  and the edges reflect the pointer structure between the
		  cells of the heap. Each cell contains a set of variables
		  which range over the natural numbers. Our method relies on
		  standard backward reachability analysis, where the main
		  idea is to use a simple set of predicates, called
		  signatures, in order to represent bad sets of heaps.
		  Examples of bad heaps are those which contain either
		  garbage, lists which are not well-formed, or lists which
		  are not sorted. We present the results for the case of
		  programs with a single next-selector, and where variables
		  may be compared for (in)equality. This allows us to verify
		  for instance that a program, like bubble sort or insertion
		  sort, returns a list which is well-formed and sorted, or
		  that the merging of two sorted lists is a new sorted list.
		  We report on the result of running a prototype based on the
		  method on a number of programs.}
}