@inproceedings{ee767142d1dc4515a9646c20e706bf28,
title = "Reasoning about pointers in refinement calculus",
abstract = "Pointers are an important programming concept. They are used explicitely or implicitly in many programming languages. In particular, the semantics of object-oriented programming languages rely on pointers. We introduce a semantics for pointer structures. Pointers are seen as indexes and pointer fields are functions from these indexes to values. Using this semantics we turn all pointer operations into simple assignments and then we use refinement calculus techniques to construct a pointer-manipulating program that checks whether or not a single linked list has a loop. We also introduce an induction principle on pointer structures in order to reduce complexity of the proofs.",
author = "Back, {Ralph Johan} and Xiaocong Fan and Viorel Preoteasa",
year = "2003",
month = jan,
day = "1",
doi = "10.1109/APSEC.2003.01254398",
language = "English (US)",
series = "Proceedings - Asia-Pacific Software Engineering Conference, APSEC",
publisher = "IEEE Computer Society",
pages = "425--434",
booktitle = "10th Asia-Pacific Software Engineering Conference, APSEC 2003",
address = "United States",
note = "10th Asia-Pacific Software Engineering Conference, APSEC 2003 ; Conference date: 10-12-2003 Through 12-12-2003",
}