Verifying spatial properties of stencil computations

Add to your list(s) Download to your calendar using vCal

• Mistral Contrastin
• Tuesday 21 March 2017, 17:05-17:30
• FW26.

If you have a question about this talk, please contact Matthew Danish.

Stencil computation is a ubiquitous programming idiom in scientific computing. It involves iterated assignments to an array from some combination of the values in the neighbourhood of the current indices of an iteration e.g. a[i][j] = a[i][j+1] + a[i][j-1] in a nested loop with i and j as induction variables. These are heavily used in scientific simulations as well as image processing algorithms.

The indexing behaviour may easily involve more than 10 terms indexing in two or three dimensions. This opens room for errors in offsets. We hypothesised that vast majority of stencil computations involve continuous and symmetrical offsets from induction variables. We present a succinct specification language that allows verifying such spatial properties.

This talk is part of the Testing & Verification For Computational Science series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Testing & Verification For Computational Science
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.