@inproceedings{dyer-correctness-2019,
author = {Dyer, Tristan and Altuntas, Alper and Baugh, John},
title = {Bounded verification of sparse matrix computations},
booktitle = {Proceedings of the Third International Workshop on
  Software Correctness for {HPC} Applications, {Correctness'19}},
year = {2019},
isbn = {978-1-7281-6015-3},
location = {Denver, CO, USA},
pages = {36-43},
doi = {10.1109/Correctness49594.2019.00010},
url_pdf = {papers/dyer-correctness-2019.pdf},
publisher = {IEEE/ACM},
keywords = {sparse matrix formats, state-based formal methods, mechanical
  verification},
abstract = {
We show how to model and reason about the structure and behavior of
sparse matrices, which are central to many applications in scientific
computation.  Our approach is state-based, relying on a formalism
called Alloy to show that one model is a refinement of another.  We
present examples of sparse matrix-vector multiplication, transpose,
and translation between formats using ELLPACK and compressed sparse
row formats to demonstrate the approach.  To model matrix computations
in a declarative language like Alloy, a new idiom is presented for
bounded iteration with incremental updates.  Mechanical verification
is performed using SAT solvers built into the tool.}
}

{"_id":"A4Yz2kR77CGNkkPSW","bibbaseid":"dyer-altuntas-baugh-boundedverificationofsparsematrixcomputations-2019","author_short":["Dyer, T.","Altuntas, A.","Baugh, J."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Dyer"],"firstnames":["Tristan"],"suffixes":[]},{"propositions":[],"lastnames":["Altuntas"],"firstnames":["Alper"],"suffixes":[]},{"propositions":[],"lastnames":["Baugh"],"firstnames":["John"],"suffixes":[]}],"title":"Bounded verification of sparse matrix computations","booktitle":"Proceedings of the Third International Workshop on Software Correctness for HPC Applications, Correctness'19","year":"2019","isbn":"978-1-7281-6015-3","location":"Denver, CO, USA","pages":"36-43","doi":"10.1109/Correctness49594.2019.00010","url_pdf":"papers/dyer-correctness-2019.pdf","publisher":"IEEE/ACM","keywords":"sparse matrix formats, state-based formal methods, mechanical verification","abstract":"We show how to model and reason about the structure and behavior of sparse matrices, which are central to many applications in scientific computation. Our approach is state-based, relying on a formalism called Alloy to show that one model is a refinement of another. We present examples of sparse matrix-vector multiplication, transpose, and translation between formats using ELLPACK and compressed sparse row formats to demonstrate the approach. To model matrix computations in a declarative language like Alloy, a new idiom is presented for bounded iteration with incremental updates. Mechanical verification is performed using SAT solvers built into the tool.","bibtex":"@inproceedings{dyer-correctness-2019,\nauthor = {Dyer, Tristan and Altuntas, Alper and Baugh, John},\ntitle = {Bounded verification of sparse matrix computations},\nbooktitle = {Proceedings of the Third International Workshop on\n Software Correctness for {HPC} Applications, {Correctness'19}},\nyear = {2019},\nisbn = {978-1-7281-6015-3},\nlocation = {Denver, CO, USA},\npages = {36-43},\ndoi = {10.1109/Correctness49594.2019.00010},\nurl_pdf = {papers/dyer-correctness-2019.pdf},\npublisher = {IEEE/ACM},\nkeywords = {sparse matrix formats, state-based formal methods, mechanical\n verification},\nabstract = {\nWe show how to model and reason about the structure and behavior of\nsparse matrices, which are central to many applications in scientific\ncomputation. Our approach is state-based, relying on a formalism\ncalled Alloy to show that one model is a refinement of another. We\npresent examples of sparse matrix-vector multiplication, transpose,\nand translation between formats using ELLPACK and compressed sparse\nrow formats to demonstrate the approach. To model matrix computations\nin a declarative language like Alloy, a new idiom is presented for\nbounded iteration with incremental updates. Mechanical verification\nis performed using SAT solvers built into the tool.}\n}\n\n","author_short":["Dyer, T.","Altuntas, A.","Baugh, J."],"key":"dyer-correctness-2019","id":"dyer-correctness-2019","bibbaseid":"dyer-altuntas-baugh-boundedverificationofsparsematrixcomputations-2019","role":"author","urls":{" pdf":"https://jwbaugh.github.io/papers/dyer-correctness-2019.pdf"},"keyword":["sparse matrix formats","state-based formal methods","mechanical verification"],"metadata":{"authorlinks":{}},"downloads":13},"bibtype":"inproceedings","biburl":"https://jwbaugh.github.io/jwb.bib","dataSources":["pewK2DSYXKNLH3TTe"],"keywords":["sparse matrix formats","state-based formal methods","mechanical verification"],"search_terms":["bounded","verification","sparse","matrix","computations","dyer","altuntas","baugh"],"title":"Bounded verification of sparse matrix computations","year":2019,"downloads":13}