What Challenges Do Developers Face When Using Verification-Aware Programming Languages?

• URL: http://arxiv.org/abs/2506.23696v2
• Date: Sun, 07 Sep 2025 11:10:45 GMT
• Title: What Challenges Do Developers Face When Using Verification-Aware Programming Languages?
• Authors: Francisco Oliveira, Alexandra Mendes, Carolina Carreira,
• Abstract summary: In software development, increasing software reliability often involves testing.<n>For complex and critical systems, developers can use Design by Contract (DbC) methods to define precise specifications that software components must satisfy.<n> Verification-Aware (VA) programming languages support DbC and formal verification at compile-time or run-time, offering stronger correctness guarantees than traditional testing.
• Score: 43.72088093637808
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Software reliability is critical in ensuring that the digital systems we depend on function correctly. In software development, increasing software reliability often involves testing. However, for complex and critical systems, developers can use Design by Contract (DbC) methods to define precise specifications that software components must satisfy. Verification-Aware (VA) programming languages support DbC and formal verification at compile-time or run-time, offering stronger correctness guarantees than traditional testing. However, despite the strong guarantees provided by VA languages, their adoption remains limited. In this study, we investigate the barriers to adopting VA languages by analyzing developer discussions on public forums using topic modeling techniques. We complement this analysis with a developer survey to better understand the practical challenges associated with VA languages. Our findings reveal key obstacles to adoption, including steep learning curves and usability issues. Based on these insights, we identify actionable recommendations to improve the usability and accessibility of VA languages. Our findings suggest that simplifying tool interfaces, providing better educational materials, and improving integration with everyday development environments could improve the usability and adoption of these languages. Our work provides actionable insights for improving the usability of VA languages and making verification tools more accessible.

Related papers

• Applying Formal Methods Tools to an Electronic Warfare Codebase (Experience report) [5.130336628792388]
  We discuss our experiences with identifying and applying formal methods tools on an electronic warfare (EW) system with stringent safety requirements.<n>We present suggestions for improving formal methods usability including better documentation of capabilities, decreased manual effort, and improved handling of library code.
  arXiv  Detail & Related papers  (2026-01-16T18:46:19Z)
• SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks [2.5374060352463697]
  SV-LIB is an exchange format and intermediate language for software-verification tasks.<n>This paper presents version 1.0 of the SV-LIBformat, including its design goals, the syntax, and informal semantics.
  arXiv  Detail & Related papers  (2025-11-26T15:44:54Z)
• Improving Large Language Models Function Calling and Interpretability via Guided-Structured Templates [56.73907811047611]
  Large language models (LLMs) have demonstrated strong reasoning and tool-use capabilities.<n>LLMs often fail in real-world tool-interactions due to incorrect parameterization, poor tool selection, or misinterpretation of user intent.<n>We introduce a curriculum-inspired framework that leverages structured reasoning templates to guide LLMs through more deliberate step-by-step instructions for generating function callings.
  arXiv  Detail & Related papers  (2025-09-22T17:55:14Z)
• On Integrating Large Language Models and Scenario-Based Programming for Improving Software Reliability [2.2058293096044586]
  Large Language Models (LLMs) are fast becoming indispensable tools for software developers.<n>LLMs often introduce significant errors and present incorrect code with persuasive confidence.<n>We propose a methodology for combining LLMs with traditional'' software engineering techniques in a structured way.
  arXiv  Detail & Related papers  (2025-09-11T07:10:25Z)
• Evaluating Language Model Reasoning about Confidential Information [95.64687778185703]
  We study whether language models exhibit contextual robustness, or the capability to adhere to context-dependent safety specifications.<n>We develop a benchmark (PasswordEval) that measures whether language models can correctly determine when a user request is authorized.<n>We find that current open- and closed-source models struggle with this seemingly simple task, and that, perhaps surprisingly, reasoning capabilities do not generally improve performance.
  arXiv  Detail & Related papers  (2025-08-27T15:39:46Z)
• NEAT: QCP: A Practical Separation Logic-based C Program Verification Tool [4.449417653464987]
  This paper introduces a novel verification tool, called textbf C Programming Verifier (QCP).<n>QCP incorporates a refined front-end %syntax of assertion language to enhance user interaction.
  arXiv  Detail & Related papers  (2025-05-19T09:04:34Z)
• Development and Adoption of SATD Detection Tools: A State-of-practice Report [5.670597842524448]
  Self-Admitted Technical Debt (SATD) refers to instances where developers knowingly introduce suboptimal solutions into code.<n>This paper provides a comprehensive state-of-practice report on the development and adoption of SATD detection tools.
  arXiv  Detail & Related papers  (2024-12-18T12:06:53Z)
• Training of Scaffolded Language Models with Language Supervision: A Survey [62.59629932720519]
  This survey organizes the literature on the design and optimization of emerging structures around post-trained LMs.<n>We refer to this overarching structure as scaffolded LMs and focus on LMs that are integrated into multi-step processes with tools.
  arXiv  Detail & Related papers  (2024-10-21T18:06:25Z)
• Multilingual Crowd-Based Requirements Engineering Using Large Language Models [9.93427497289912]
  We present an LLM-powered approach that helps agile teams use crowd-based requirements engineering (CrowdRE) in their issue and task management. We are currently implementing a command-line tool that enables developers to match issues with relevant user reviews.
  arXiv  Detail & Related papers  (2024-08-12T21:40:39Z)
• DIALIGHT: Lightweight Multilingual Development and Evaluation of Task-Oriented Dialogue Systems with Large Language Models [76.79929883963275]
  DIALIGHT is a toolkit for developing and evaluating multilingual Task-Oriented Dialogue (ToD) systems. It features a secure, user-friendly web interface for fine-grained human evaluation at both local utterance level and global dialogue level. Our evaluations reveal that while PLM fine-tuning leads to higher accuracy and coherence, LLM-based systems excel in producing diverse and likeable responses.
  arXiv  Detail & Related papers  (2024-01-04T11:27:48Z)
• AdaCCD: Adaptive Semantic Contrasts Discovery Based Cross Lingual Adaptation for Code Clone Detection [69.79627042058048]
  AdaCCD is a novel cross-lingual adaptation method that can detect cloned codes in a new language without annotations in that language. We evaluate the cross-lingual adaptation results of AdaCCD by constructing a multilingual code clone detection benchmark consisting of 5 programming languages.
  arXiv  Detail & Related papers  (2023-11-13T12:20:48Z)
• ChatDev: Communicative Agents for Software Development [84.90400377131962]
  ChatDev is a chat-powered software development framework in which specialized agents are guided in what to communicate. These agents actively contribute to the design, coding, and testing phases through unified language-based communication.
  arXiv  Detail & Related papers  (2023-07-16T02:11:34Z)
• AIBugHunter: A Practical Tool for Predicting, Classifying and Repairing Software Vulnerabilities [27.891905729536372]
  AIBugHunter is a novel ML-based software vulnerability analysis tool for C/C++ languages that is integrated into Visual Studio Code. We propose a novel multi-objective optimization (MOO)-based vulnerability classification approach and a transformer-based estimation approach to help AIBugHunter accurately identify vulnerability types and estimate severity.
  arXiv  Detail & Related papers  (2023-05-26T04:21:53Z)
• MLSmellHound: A Context-Aware Code Analysis Tool [4.157846027410602]
  Code analysis tools must account for the cultural differences within the teams which manifests as multiple programming languages. Existing tools fail to identify these cultural differences and are geared towards software engineering which reduces their adoption in machine learning projects. In our approach we attempt to resolve this problem by exploring the use of context which includes i) purpose of the source code, ii) technical domain,iii) problem domain, iv) team norms, v) development lifecycle stage. This allows for contextualised and meaningful error reporting for the end-user.
  arXiv  Detail & Related papers  (2022-05-08T06:01:22Z)
• AVATAR: A Parallel Corpus for Java-Python Program Translation [77.86173793901139]
  Program translation refers to migrating source code from one language to another. We present AVATAR, a collection of 9,515 programming problems and their solutions written in two popular languages, Java and Python.
  arXiv  Detail & Related papers  (2021-08-26T05:44:20Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.