Title: Verifying a Sparse Matrix Algorithm Using Symbolic Execution
Author: Alex Wilton

Abstract:

Scientific software is, by its very nature, complex. It is
mathematical and highly optimized which makes it prone to subtle bugs
not as easily detected by traditional testing. We outline how symbolic
execution can be used to write tests similar to traditional unit tests
while providing stronger verification guarantees and apply this
methodology to a sparse matrix algorithm.