Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Toward Practical Deductive Verification: Insights from a Qualitative Survey in Industry and Academia

Lea Salome Brugger, Xavier Denis, Peter Müller

TL;DR

This paper addresses the challenge of making deductive verification a mainstream practice by conducting a qualitative study based on semi-structured interviews with 30 practitioners from industry and academia. Using thematic analysis, it identifies four key success factors and five major barriers, highlighting underexplored issues such as proof maintenance and the tension between automation and user control. The authors translate these findings into practical recommendations for practitioners, tool builders, and researchers, emphasizing early integration, focus on critical components, usability, and workflow integration. The work provides a nuanced, evidence-based roadmap for improving tooling, pedagogy, and integration strategies to broaden the adoption of deductive verification in real-world settings.

Abstract

Deductive verification is an effective method to ensure that a given system exposes the intended behavior. In spite of its proven usefulness and feasibility in selected projects, deductive verification is still not a mainstream technique. To pave the way to widespread use, we present a study investigating the factors enabling successful applications of deductive verification and the underlying issues preventing broader adoption. We conducted semi-structured interviews with 30 practitioners of verification from both industry and academia and systematically analyzed the collected data employing a thematic analysis approach. Beside empirically confirming familiar challenges, e.g., the high level of expertise needed for conducting formal proofs, our data reveal several underexplored obstacles, such as proof maintenance, insufficient control over automation, and usability concerns. We further use the results from our data analysis to extract enablers and barriers for deductive verification and formulate concrete recommendations for practitioners, tool builders, and researchers, including principles for usability, automation, and integration with existing workflows.

Toward Practical Deductive Verification: Insights from a Qualitative Survey in Industry and Academia

TL;DR

This paper addresses the challenge of making deductive verification a mainstream practice by conducting a qualitative study based on semi-structured interviews with 30 practitioners from industry and academia. Using thematic analysis, it identifies four key success factors and five major barriers, highlighting underexplored issues such as proof maintenance and the tension between automation and user control. The authors translate these findings into practical recommendations for practitioners, tool builders, and researchers, emphasizing early integration, focus on critical components, usability, and workflow integration. The work provides a nuanced, evidence-based roadmap for improving tooling, pedagogy, and integration strategies to broaden the adoption of deductive verification in real-world settings.

Abstract

Deductive verification is an effective method to ensure that a given system exposes the intended behavior. In spite of its proven usefulness and feasibility in selected projects, deductive verification is still not a mainstream technique. To pave the way to widespread use, we present a study investigating the factors enabling successful applications of deductive verification and the underlying issues preventing broader adoption. We conducted semi-structured interviews with 30 practitioners of verification from both industry and academia and systematically analyzed the collected data employing a thematic analysis approach. Beside empirically confirming familiar challenges, e.g., the high level of expertise needed for conducting formal proofs, our data reveal several underexplored obstacles, such as proof maintenance, insufficient control over automation, and usability concerns. We further use the results from our data analysis to extract enablers and barriers for deductive verification and formulate concrete recommendations for practitioners, tool builders, and researchers, including principles for usability, automation, and integration with existing workflows.
Paper Structure (38 sections, 1 figure, 2 tables)

This paper contains 38 sections, 1 figure, 2 tables.

Table of Contents

  1. Introduction
  2. Methodology
  3. Participants
  4. Interviews
  5. Data Analysis
  6. Threats to Validity
  7. Results
  8. Verification Applicability
  9. Benefits of Verification
  10. Cost-Benefit Assessment Patterns
  11. Domain Selection Criteria
  12. Managing Technical Complexity
  13. Fundamental Challenges
  14. Proof Strategy
  15. Specification Engineering
  16. ...and 23 more sections

Figures (1)

  • Figure 1: Results from the pre-interview questionnaire.