Formal Verification of Parallel Prefix Sum

Formal Verification of Parallel Prefix Sum. Safari, M., Oortwijn, W., Joosten, S., & Huisman, M. In Lee, R., Jha, S., & Mavridou, A., editors, NASA Formal Methods, pages 170–186, Cham, 2020. Springer International Publishing.

Paper abstract bibtex 4 downloads

With the advent of dedicated hardware for multicore programming, parallel algorithms have become omnipresent. For example, various algorithms have been proposed for the parallel computation of a prefix sum in the literature. As the prefix sum is a basic building block for many other multicore algorithms, such as sorting, its correctness is of utmost importance. This means, the algorithm should be functionally correct, and the implementation should be thread and memory safe.

@InProceedings{10.1007/978-3-030-55754-6_10,
author="Safari, Mohsen
and Oortwijn, Wytse
and Joosten, Sebastiaan
and Huisman, Marieke",
editor="Lee, Ritchie
and Jha, Susmit
and Mavridou, Anastasia",
title="Formal Verification of Parallel Prefix Sum",
booktitle="NASA Formal Methods",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="170--186",
abstract="With the advent of dedicated hardware for multicore programming, parallel algorithms have become omnipresent. For example, various algorithms have been proposed for the parallel computation of a prefix sum in the literature. As the prefix sum is a basic building block for many other multicore algorithms, such as sorting, its correctness is of utmost importance. This means, the algorithm should be functionally correct, and the implementation should be thread and memory safe.",
isbn="978-3-030-55754-6",
url="https://doi.org/10.1007/978-3-030-55754-6_10"
}

Downloads: 4

{"_id":"7q7EnuRvaKhzTGbxm","bibbaseid":"safari-oortwijn-joosten-huisman-formalverificationofparallelprefixsum-2020","authorIDs":[],"author_short":["Safari, M.","Oortwijn, W.","Joosten, S.","Huisman, M."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Safari"],"firstnames":["Mohsen"],"suffixes":[]},{"propositions":[],"lastnames":["Oortwijn"],"firstnames":["Wytse"],"suffixes":[]},{"propositions":[],"lastnames":["Joosten"],"firstnames":["Sebastiaan"],"suffixes":[]},{"propositions":[],"lastnames":["Huisman"],"firstnames":["Marieke"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Lee"],"firstnames":["Ritchie"],"suffixes":[]},{"propositions":[],"lastnames":["Jha"],"firstnames":["Susmit"],"suffixes":[]},{"propositions":[],"lastnames":["Mavridou"],"firstnames":["Anastasia"],"suffixes":[]}],"title":"Formal Verification of Parallel Prefix Sum","booktitle":"NASA Formal Methods","year":"2020","publisher":"Springer International Publishing","address":"Cham","pages":"170–186","abstract":"With the advent of dedicated hardware for multicore programming, parallel algorithms have become omnipresent. For example, various algorithms have been proposed for the parallel computation of a prefix sum in the literature. As the prefix sum is a basic building block for many other multicore algorithms, such as sorting, its correctness is of utmost importance. This means, the algorithm should be functionally correct, and the implementation should be thread and memory safe.","isbn":"978-3-030-55754-6","url":"https://doi.org/10.1007/978-3-030-55754-6_10","bibtex":"@InProceedings{10.1007/978-3-030-55754-6_10,\nauthor=\"Safari, Mohsen\nand Oortwijn, Wytse\nand Joosten, Sebastiaan\nand Huisman, Marieke\",\neditor=\"Lee, Ritchie\nand Jha, Susmit\nand Mavridou, Anastasia\",\ntitle=\"Formal Verification of Parallel Prefix Sum\",\nbooktitle=\"NASA Formal Methods\",\nyear=\"2020\",\npublisher=\"Springer International Publishing\",\naddress=\"Cham\",\npages=\"170--186\",\nabstract=\"With the advent of dedicated hardware for multicore programming, parallel algorithms have become omnipresent. For example, various algorithms have been proposed for the parallel computation of a prefix sum in the literature. As the prefix sum is a basic building block for many other multicore algorithms, such as sorting, its correctness is of utmost importance. This means, the algorithm should be functionally correct, and the implementation should be thread and memory safe.\",\nisbn=\"978-3-030-55754-6\",\nurl=\"https://doi.org/10.1007/978-3-030-55754-6_10\"\n}\n\n\n","author_short":["Safari, M.","Oortwijn, W.","Joosten, S.","Huisman, M."],"editor_short":["Lee, R.","Jha, S.","Mavridou, A."],"key":"10.1007/978-3-030-55754-6_10","id":"10.1007/978-3-030-55754-6_10","bibbaseid":"safari-oortwijn-joosten-huisman-formalverificationofparallelprefixsum-2020","role":"author","urls":{"Paper":"https://doi.org/10.1007/978-3-030-55754-6_10"},"metadata":{"authorlinks":{}},"downloads":4,"html":""},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","creationDate":"2020-03-11T13:41:07.969Z","downloads":4,"keywords":[],"search_terms":["formal","verification","parallel","prefix","sum","safari","oortwijn","joosten","huisman"],"title":"Formal Verification of Parallel Prefix Sum","year":2020,"dataSources":["2tJugFYAignELAmZo","zT4KxAXTKvhK2Hrr4","cCvCnPTRQYq3qPe9y"]}