Specifying and verifying sparse matrix codes

DOI10.1145/1863543.1863581MaRDI QIDQ5176944zbMATH OpenOpenAlexFDO

Authors Gilad Arnold, Johannes Hölzl, Ali Sinan Köksal, Rastislav Bodík, Mooly Sagiv

Publication date 5 March 2015

Published in Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1863543.1863581

zbMATH Keywords

sparse matrix codesverification

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1760021
• Static analysis by abstract interpretation of the functional correctness of matrix manipulating programs
• Publication:4730673
• Inferring functional properties of matrix manipulating programs by abstract interpretation
• The matrix reproved (verification pearl)

Cited in

(2)

• Verification of the Redecoration Algorithm for Triangular Matrices
• Good codes based on very sparse matrices

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Specifying and verifying sparse matrix codes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5176944)