What Challenges Do Developers Face When Using Verification-Aware Programming Languages?
- URL: http://arxiv.org/abs/2506.23696v1
- Date: Mon, 30 Jun 2025 10:17:39 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: 45.44831696628473
- 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
- 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.