Proving properties of multidimensional recurrences with application to regular parallel algorithms
David Cachera, Patrice Quinton, Sanjay V. Rajopadhye, Tanguy Risset · 2005
We present a set of verification methods to prove properties of parallel systems described by means of multidimensional affine recurrence equations. We use polyhedral analysis and transformation techniques together with theorem proving. Polyhedral techniques allow us to handle simple but otherwise costly proof steps, while theorem proving provides more expressivity and more complex proof techniques. This allows large, generic and structured systems to be verified. These methods are implemented in the M-MAlpha environment using the PVS theorem prover. 1