Proofs for ‘Verifying Spatial Properties of Array Computations’

Dominic Orchard, Mistral Contrastin, Matthew Danish & Andrew Rice
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...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.