@TechReport{	  it:2008-015,
  author	= {Parosh Aziz Abdulla and Ahmed Bouajjani and Jonathan
		  Cederberg and Fr{\'e}d{\'e}ric Haziza and Ahmed Rezine},
  title		= {Monotonic Abstraction for Programs with Dynamic Memory
		  Heaps},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Division of Computer Systems},
  year		= {2008},
  number	= {2008-015},
  optmonth	= {},
  abstract	= {We propose a new approach for automatic verification of
		  programs with dynamic heap manipulation. The method is
		  based on symbolic (backward) reachability analysis using
		  upward-closed sets of heaps w.r.t. an appropriate preorder
		  on graphs. These sets are represented by a finite set of
		  minimal graph patterns corresponding to a set of bad
		  configurations. We define an abstract semantics for the
		  programs which is monotonic w.r.t. the preorder. Moreover,
		  we prove that our analysis always terminates by showing
		  that the preorder is a well-quasi ordering. Our results are
		  presented for the case of programs with 1-next selector. We
		  provide experimental results showing the effectiveness of
		  our approach. }
}