- Restrictions on Access:
- Unclassified, Unlimited, Publicly available.
- 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.
- NASA Technical Reports Server (NTRS) Collection.
- Document ID: 20150011436.
International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2014); 9-11 Sep. 2014; Canterbury; United Kingdom.
- Copyright, Distribution under U.S. Government purpose rights.
View MARC record | catkey: 17532502