A Unit Proofing Framework for Code-level Verification: A Research Agenda
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915266170978304 |
|---|---|
| author | Amusuo, Paschal C. Patil, Parth V. Cochell, Owen Lievre, Taylor Le Davis, James C. |
| author_facet | Amusuo, Paschal C. Patil, Parth V. Cochell, Owen Lievre, Taylor Le Davis, James C. |
| contents | Formal verification provides mathematical guarantees that a software is correct. Design-level verification tools ensure software specifications are correct, but they do not expose defects in actual implementations. For this purpose, engineers use code-level tools. However, such tools struggle to scale to large software. The process of "Unit Proofing" mitigates this by decomposing the software and verifying each unit independently. We examined AWS's use of unit proofing and observed that current approaches are manual and prone to faults that mask severe defects. We propose a research agenda for a unit proofing framework, both methods and tools, to support software engineers in applying unit proofing effectively and efficiently. This will enable engineers to discover code-level defects early. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_14818 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Unit Proofing Framework for Code-level Verification: A Research Agenda Amusuo, Paschal C. Patil, Parth V. Cochell, Owen Lievre, Taylor Le Davis, James C. Software Engineering D.2.4; F.3.1 Formal verification provides mathematical guarantees that a software is correct. Design-level verification tools ensure software specifications are correct, but they do not expose defects in actual implementations. For this purpose, engineers use code-level tools. However, such tools struggle to scale to large software. The process of "Unit Proofing" mitigates this by decomposing the software and verifying each unit independently. We examined AWS's use of unit proofing and observed that current approaches are manual and prone to faults that mask severe defects. We propose a research agenda for a unit proofing framework, both methods and tools, to support software engineers in applying unit proofing effectively and efficiently. This will enable engineers to discover code-level defects early. |
| title | A Unit Proofing Framework for Code-level Verification: A Research Agenda |
| topic | Software Engineering D.2.4; F.3.1 |
| url | https://arxiv.org/abs/2410.14818 |