### Skapa referens, olika format (klipp och klistra)

**Harvard**

Ji, R., Abdulla, P., Cederberg, J. och Atto, M. (2009) *Automated Analysis of Data-Dependent Programs with Dynamic Memory*.

** BibTeX **

@conference{

Ji2009,

author={Ji, Ran and Abdulla, Parosh Aziz and Cederberg, Jonathan and Atto, Muhsin},

title={Automated Analysis of Data-Dependent Programs with Dynamic Memory},

booktitle={Proc. 7th International Symposium on Automated Technology for Verification and Analysis},

isbn={978-3-642-04760-2},

pages={197-212},

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.},

year={2009},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 104091

A1 Ji, Ran

A1 Abdulla, Parosh Aziz

A1 Cederberg, Jonathan

A1 Atto, Muhsin

T1 Automated Analysis of Data-Dependent Programs with Dynamic Memory

YR 2009

T2 Proc. 7th International Symposium on Automated Technology for Verification and Analysis

SN 978-3-642-04760-2

SP 197

OP 212

AB 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.

LA eng

LK http://www.springerlink.com/content/t4745463175h2134/

OL 30