Technical reports

Proofs for ‘Verifying Spatial Properties of Array Computations’

Dominic Orchard, Mistral Contrastin, Matthew Danish, Andrew Rice

September 2017, 8 pages

DOI: 10.48456/tr-911

Abstract

This technical report provides accompanying proofs for the paper: Verifying Spatial Properties of Array Computations. We show three properties of the lattice model of the stencil specification language. 1) that it is sound with respect to the equational theory of region specifications; 2) that is it sound with respect to the theory of region approximation; 3) that the inference algorithm is sound. We further derive useful identities on the specification language and properties of Union Normal Form—the data structure used to implement the model. Core definitions from the paper are restated here to make the overall report more self contained.

Full text

PDF (0.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-911,
  author =	 {Orchard, Dominic and Contrastin, Mistral and Danish,
          	  Matthew and Rice, Andrew},
  title = 	 {{Proofs for `Verifying Spatial Properties of Array
         	   Computations'}},
  year = 	 2017,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-911.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-911},
  number = 	 {UCAM-CL-TR-911}
}