Awesome

graphblas-verif

*** THIS README AND REPOSITORY ARE WORKS IN PROGRESS: Mostly finalized versions will be available after August 24, 2018 ***

Formal verification of the GraphBLAS C API implementation by Tim Davis using Frama-C/WP and VeriFast (potentially). Modified versions of GraphBLAS 2.0.1 (for verification) are contained within this repository as well as an unmodified version for comparison.

For those interested, the most recent version of GraphBLAS is packaged with SuiteSparse and can be downloaded here.

Documentation

For more information and documentation, please visit the Wiki.

Acknowledgments

Mentors

• Manoj Kumar, IBM Research
• Jonathan Aldrich, Carnegie Mellon University
• Joshua Sunshine, Carnegie Mellon University
• Pratap Pattniak, IBM Research

We would like to thank Tim Davis (Texas A&M University) for allowing the use, modification, and distribution of his GraphBLAS implementation.

We would also like to thank IBM for funding this research.