Analyzing array manipulating programs by program transformation

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

doi:10.1007/978-3-319-17822-6_1

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 proceeding › Conference Paper › Research › peer-review

5 Citations (Scopus)

Abstract

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 language	English
Title of host publication	Logic-Based Program Synthesis and Transformation
Subtitle of host publication	24th International Symposium, LOPSTR 2014 Canterbury, UK, September 9–11, 2014 Revised Selected Papers
Editors	Maurizio Proietti, Hirohisa Seki
Place of Publication	Cham Switzerland
Publisher	Springer
Pages	3-20
Number of pages	18
ISBN (Electronic)	9783319178226
ISBN (Print)	9783319178219
DOIs	https://doi.org/10.1007/978-3-319-17822-6_1
Publication status	Published - 2015
Externally published	Yes
Event	International Symposium on Logic-Based Program Synthesis and Transformation 2014 - Canterbury, United Kingdom Duration: 9 Sept 2014 → 11 Sept 2014 Conference number: 24th http://www.iasi.cnr.it/events/lopstr14/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	8981
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Symposium on Logic-Based Program Synthesis and Transformation 2014
Abbreviated title	LOPSTR 2014
Country/Territory	United Kingdom
City	Canterbury
Period	9/09/14 → 11/09/14
Internet address	http://www.iasi.cnr.it/events/lopstr14/

Access to Document

10.1007/978-3-319-17822-6_1

Cite this

Cornish, J. R. M., Gange, G., Navas, J. A., Schachte, P., Søndergaard, H., & Stuckey, P. J. (2015). Analyzing array manipulating programs by program transformation. In M. Proietti, & H. Seki (Eds.), Logic-Based Program Synthesis and Transformation: 24th International Symposium, LOPSTR 2014 Canterbury, UK, September 9–11, 2014 Revised Selected Papers (pp. 3-20). (Lecture Notes in Computer Science ; Vol. 8981). Springer. https://doi.org/10.1007/978-3-319-17822-6_1

Cornish, J. Robert M. ; Gange, Graeme ; Navas, Jorge A. et al. / Analyzing array manipulating programs by program transformation. Logic-Based Program Synthesis and Transformation: 24th International Symposium, LOPSTR 2014 Canterbury, UK, September 9–11, 2014 Revised Selected Papers. editor / Maurizio Proietti ; Hirohisa Seki. Cham Switzerland : Springer, 2015. pp. 3-20 (Lecture Notes in Computer Science ).

@inproceedings{ca215faf742c44e4985d0d7d82e6368f,

title = "Analyzing array manipulating programs by program transformation",

abstract = "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.",

author = "Cornish, \{J. Robert M.\} and Graeme Gange and Navas, \{Jorge A.\} and Peter Schachte and Harald S{\o}ndergaard and Stuckey, \{Peter J.\}",

year = "2015",

doi = "10.1007/978-3-319-17822-6\_1",

language = "English",

isbn = "9783319178219",

series = "Lecture Notes in Computer Science ",

publisher = "Springer",

pages = "3--20",

editor = "Maurizio Proietti and Hirohisa Seki",

booktitle = "Logic-Based Program Synthesis and Transformation",

address = "Switzerland",

note = "International Symposium on Logic-Based Program Synthesis and Transformation 2014, LOPSTR 2014 ; Conference date: 09-09-2014 Through 11-09-2014",

url = "http://www.iasi.cnr.it/events/lopstr14/",

}

Cornish, JRM, Gange, G, Navas, JA, Schachte, P, Søndergaard, H & Stuckey, PJ 2015, Analyzing array manipulating programs by program transformation. in M Proietti & H Seki (eds), Logic-Based Program Synthesis and Transformation: 24th International Symposium, LOPSTR 2014 Canterbury, UK, September 9–11, 2014 Revised Selected Papers. Lecture Notes in Computer Science , vol. 8981, Springer, Cham Switzerland , pp. 3-20, International Symposium on Logic-Based Program Synthesis and Transformation 2014, Canterbury, United Kingdom, 9/09/14. https://doi.org/10.1007/978-3-319-17822-6_1

Analyzing array manipulating programs by program transformation. / Cornish, J. Robert M.; Gange, Graeme; Navas, Jorge A. et al.
Logic-Based Program Synthesis and Transformation: 24th International Symposium, LOPSTR 2014 Canterbury, UK, September 9–11, 2014 Revised Selected Papers. ed. / Maurizio Proietti; Hirohisa Seki. Cham Switzerland : Springer, 2015. p. 3-20 (Lecture Notes in Computer Science ; Vol. 8981).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - Analyzing array manipulating programs by program transformation

AU - Cornish, J. Robert M.

AU - Gange, Graeme

AU - Navas, Jorge A.

AU - Schachte, Peter

AU - Søndergaard, Harald

AU - Stuckey, Peter J.

N1 - Conference code: 24th

PY - 2015

Y1 - 2015

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

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

UR - https://www.scopus.com/pages/publications/84942526165

U2 - 10.1007/978-3-319-17822-6_1

DO - 10.1007/978-3-319-17822-6_1

M3 - Conference Paper

AN - SCOPUS:84942526165

SN - 9783319178219

T3 - Lecture Notes in Computer Science

SP - 3

EP - 20

BT - Logic-Based Program Synthesis and Transformation

A2 - Proietti, Maurizio

A2 - Seki, Hirohisa

PB - Springer

CY - Cham Switzerland

T2 - International Symposium on Logic-Based Program Synthesis and Transformation 2014

Y2 - 9 September 2014 through 11 September 2014

ER -

Cornish JRM, Gange G, Navas JA, Schachte P, Søndergaard H, Stuckey PJ. Analyzing array manipulating programs by program transformation. In Proietti M, Seki H, editors, Logic-Based Program Synthesis and Transformation: 24th International Symposium, LOPSTR 2014 Canterbury, UK, September 9–11, 2014 Revised Selected Papers. Cham Switzerland : Springer. 2015. p. 3-20. (Lecture Notes in Computer Science ). doi: 10.1007/978-3-319-17822-6_1

Analyzing array manipulating programs by program transformation

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this