NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
Analyzing Array Manipulating Programs by Program TransformationWe 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.
Document ID
20150011436
Acquisition Source
Ames Research Center
Document Type
Conference Paper
Authors
Cornish, J. Robert M. (Melbourne Univ. Victoria, Australia)
Gange, Graeme (Melbourne Univ. Victoria, Australia)
Navas, Jorge A. (Stinger Ghaffarian Technologies, Inc. (SGT, Inc.) Moffett Field, CA, United States)
Schachte, Peter (Melbourne Univ. Victoria, Australia)
Sondergaard, Harald (Melbourne Univ. Victoria, Australia)
Stuckey, Peter J. (Melbourne Univ. Victoria, Australia)
Date Acquired
June 23, 2015
Publication Date
September 9, 2014
Subject Category
Computer Programming And Software
Report/Patent Number
ARC-E-DAA-TN19460
Meeting Information
Meeting: International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2014)
Location: Canterbury
Country: United Kingdom
Start Date: September 9, 2014
End Date: September 11, 2014
Sponsors: Kent Univ., Consiglio Nazionale delle Ricerche
Funding Number(s)
CONTRACT_GRANT: DP140102194
CONTRACT_GRANT: NNA14AA60C
Distribution Limits
Public
Copyright
Public Use Permitted.
Keywords
Program Transformation
Abstract Interpretation
Array Content Analysis

Related Records

There are no records associated with this record.
No Preview Available