A Pyramid Of (Formal) Software Verification
Brain, M. ORCID: 0000-0003-4216-7151 & Polgreen, E. (2024). A Pyramid Of (Formal) Software Verification. Paper presented at the 26th International Symposium, FM 2024, 9-13 Sep 2024, Milan, Italy. doi: 10.1007/978-3-031-71177-0_24
Abstract
Over the past few years there has been significant progress in the various fields of software verification resulting in many useful tools and successful deployments, both academic and commercial. However much of the work describing these tools and ideas is written by and for the research community. The scale, diversity and focus of the literature can act as a barrier, separating industrial users and the wider academic community from the tools that could make their work more efficient, more certain and more productive. This tutorial gives a simple classification of verification techniques in terms of a pyramid and uses it to describe the six main schools of verification technologies. We have found this approach valuable for building collaborations with industry as it allows us to explain the intrinsic strengths and weaknesses of techniques and pick the right tool for any given industrial application. The model also highlights some of the cultural differences and unspoken assumptions of different areas of verification and illuminates future directions.
Publication Type: | Conference or Workshop Item (Paper) |
---|---|
Additional Information: | This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. |
Subjects: | Q Science > QA Mathematics > QA75 Electronic computers. Computer science |
Departments: | School of Science & Technology School of Science & Technology > Computer Science |
SWORD Depositor: |
Available under License Creative Commons: Attribution International Public License 4.0.
Download (751kB) | Preview
Export
Downloads
Downloads per month over past year