[OOPSLA'25] On the Impact of Formal Verification on Software Development

Описание: On the Impact of Formal Verification on Software Development (Video, OOPSLA2 2025)
Eric Mugnier, Yuanyuan Zhou, Ranjit Jhala, and Michael Coblenz
(University of California at San Diego, USA; University of California at San Diego, USA; University of California at San Diego, USA; University of California at San Diego, USA)

Abstract: Auto-active verifiers like Dafny aim to make formal methods accessible to non-expert users through SMT automation. However, despite the automation and other programmer-friendly features, they remain sparsely used in real-world software development, due to the significant effort required to apply them in practice. We interviewed 14 experienced Dafny users about their experiences using it in large-scale projects. We apply grounded theory to analyze the interviews to systematically identify how auto-active verification impacts software development, and to identify opportunities to simplify the use, and hence, expand the adoption of verification in software development.

Article: https://doi.org/10.1145/3763181

Supplementary archive: https://doi.org/10.5281/zenodo.15761040 (Badges: Artifacts Available)

ORCID: https://orcid.org/0009-0006-4967-6820, https://orcid.org/0009-0006-0980-2538, https://orcid.org/0000-0002-1802-9421, https://orcid.org/0000-0002-9369-4069

Video Tags: User study, Dafny, Grounded theory, oopslab25main-p1467-p, doi:10.1145/3763181, doi:10.5281/zenodo.15761040, orcid:0009-0006-4967-6820, orcid:0009-0006-0980-2538, orcid:0000-0002-1802-9421, orcid:0000-0002-9369-4069, Artifacts Available

Presentation at the OOPSLA2 2025 conference, October 12–18, https://2025.splashcon.org/track/OOPSLA
Sponsored by ACM SIGPLAN,