Verifying a Sparse Matrix Algorithm Using Symbolic Execution
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915555793960960 |
|---|---|
| author | Wilton, Alexander C. |
| author_facet | Wilton, Alexander C. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_13424 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Verifying a Sparse Matrix Algorithm Using Symbolic Execution Wilton, Alexander C. Software Engineering D.2.5; G.1.3 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. |
| title | Verifying a Sparse Matrix Algorithm Using Symbolic Execution |
| topic | Software Engineering D.2.5; G.1.3 |
| url | https://arxiv.org/abs/2510.13424 |