Analyzing array manipulating programs by program transformation

J. Robert M. Cornish, Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

3 Citations (Scopus)


We explore a transformational approach to the problem of verifying simple array-manipulating programs. Traditionally, verification of such programs requires intricate analysis machinery to reason with universally quantified statements about symbolic array segments, such as “every data item stored in the segment A[i] to A[j] is equal to the corresponding item stored in the segment B[i] to B[j].”We define a simple abstract machine which allows for set-valued variables and we show how to translate programs with array operations to array-free code for this machine. For the purpose of program analysis, the translated program remains faithful to the semantics of array manipulation. Based on our implementation in LLVM, we evaluate the approach with respect to its ability to extract useful invariants and the cost in terms of code size.

Original languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation
Subtitle of host publication24th International Symposium, LOPSTR 2014 Canterbury, UK, September 9–11, 2014 Revised Selected Papers
EditorsMaurizio Proietti, Hirohisa Seki
Place of PublicationCham Switzerland
Number of pages18
ISBN (Electronic)9783319178226
ISBN (Print)9783319178219
Publication statusPublished - 2015
Externally publishedYes
EventInternational Symposium on Logic-Based Program Synthesis and Transformation 2014 - Canterbury, United Kingdom
Duration: 9 Sep 201411 Sep 2014
Conference number: 24th

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Symposium on Logic-Based Program Synthesis and Transformation 2014
Abbreviated titleLOPSTR 2014
CountryUnited Kingdom
Internet address

Cite this