Show simple item record

dc.contributor.authorAboul-Hosn, Kamalen_US
dc.date.accessioned2007-04-04T20:22:20Z
dc.date.available2007-04-04T20:22:20Z
dc.date.issued2006-05-31en_US
dc.identifier.citationhttp://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2006-2030en_US
dc.identifier.urihttps://hdl.handle.net/1813/5729
dc.description.abstractThe formal analysis of programs with arrays is a notoriously difficult problem due largely to aliasing considerations. In this paper we augment the rules of Kleene algebra with tests (KAT) with rules for the equational manipulation of arrays in the style of schematic KAT. These rules capture and make explicit the essence of subscript aliasing, where two array accesses can be to the same element. We prove the soundness of our rules, as well as illustrate their usefulness with several examples, including a complete proof of the correctness of heapsort.en_US
dc.format.extent304622 bytes
dc.format.mimetypeapplication/pdf
dc.language.isoen_USen_US
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleAn Axiomatization of Arrays for Kleene Algebra with Testsen_US
dc.typetechnical reporten_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

Statistics