Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2609.29713

DSpec2Test: Specification-Driven Test Generation in Dafny

Sofia Vieira Pinto·Álvaro F. Silva·João Pascoal Faria·Alexandra Mendes
View original source ↗Read source document ↗Export metadata ↓

Abstract

Verification-aware languages, such as Dafny, integrate logical constructs into code and enable automatic verification of program correctness. However, tests remain helpful in scenarios that verification alone does not address (e.g., to support test-driven development). Existing Dafny test generation tools are implementation-based, limiting their applicability in this context. We present DSpec2Test, a specification-driven test generation tool for Dafny that automatically derives tests from formal specifications, without considering implementation details. Our tool extends Dafny's generate-tests command with a new blackbox mode based on Disjunctive Normal Form (DNF) equivalence class partitioning and optional Boundary Value Analysis (BVA). DSpec2Test relies on the Z3 SMT solver to synthesize inputs and expected outputs that meet the specification-derived constraints. We evaluate DSpec2Test on programs from DafnyBench mutated using MutDafny and compare it against Dafny's existing implementation-driven Block mode. DSpec2Test achieves a 93.9% mutation kill rate on a dataset of 131 mutants, outperforming Block's 82.4%, and uniquely killing 17 mutants. These results suggest that specification-driven testing is an effective and complementary approach for testing Dafny programs.

Explore related subjects

cs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Sofia Vieira Pinto, Álvaro F. Silva, João Pascoal Faria, Alexandra Mendes. 2026-08-31. DSpec2Test: Specification-Driven Test Generation in Dafny. https://arxiv.org/abs/2609.29713

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Enhancing Knowledge Density via Hierarchical Context Pruning for Retrieval-Augmented Repository-Level Code Completion

Retrieval-Augmented Generation (RAG) has advanced repository-level code completion by retrieving external code snippets, API documentation, or type definitions to expand the model's contextual awareness. However, under the finite token budget of the context window, existing retrieval-augmented methods often saturate the budget with highly similar or even redundant code, which not only wastes tokens but also suppresses critical cross-file dependencies, preventing synergistic interaction between semantically similar reference snippets and cross-file dependency definitions. Therefore, further gains are limited by low knowledge density in the retrieved context rather than by model capacity. We propose SaraCoder, a retrieval-augmented framework that enhances knowledge density via hierarchical context pruning under a fixed context budget. A Hierarchical Feature Optimization module prunes an over-complete candidate pool in four stages. The freed tokens are then allocated to an External-Aware Identifier Disambiguator, which selectively injects only the most necessary cross-file dependency definitions. SaraCoder transforms context construction into a budget-aware optimization problem, balancing reference snippets and cross-file dependencies to build a context that is both knowledge-dense and semantically complete. Experiments on CrossCodeEval and RepoEval-Updated, across multiple backbone code LLMs, show that SaraCoder consistently outperforms strong RAG baselines such as GraphCoder and Repocoder in both code-level and identifier-level metrics, without increasing token usage, and yields synergistic gains when combined with other cross-file methods.

cs.SE↗
arXiv2026

Multi-LLM Orchestration for High-Quality Code Generation: Exploiting Complementary Model Strengths

Large Language Models (LLMs) are central to automated code generation, yet most approaches use one model at every stage, from writing code to repairing and optimizing it. LLMs have complementary strengths: their failures do not fully overlap across programming languages, algorithmic categories, and development stages. For example, in Python, the model with the highest code-generation accuracy ranks last at code repair. Using one model to generate code, another to repair it, and a third to refine it can therefore achieve higher correctness and better execution performance than a single model throughout. We propose PerfOrch, a multi-LLM multi-agent system with four agents for categorization, generation, debugging, and refinement. The generation, debugging, and refinement agents select models through a Memory module that ranks candidate LLMs by their measured performance for each stage, programming language, and algorithmic category. We evaluate PerfOrch with five candidate LLMs on 4,640 problems from four benchmarks covering five programming languages (HumanEval-X, EffiBench-X, BigCodeBench, and APPS) against single-model direct generation, single-model generate-debug-refine pipelines (PerfCodeGen), and the state-of-the-art multi-agent systems MapCoder and CodeSIM. PerfOrch achieves the highest pass@1 in all twelve benchmark-language settings, exceeding the strongest baseline by an average of 8.19 percentage points, and reduces execution time for an average of 75.03% of solved problems with an average speedup of 1.18x. The Memory rankings remain effective on three unseen benchmarks without re-profiling. Sequential refinement matches exhaustive execution-time refinement coverage with 66% fewer refinement-stage tokens (57% for average-memory optimization). The complementary strengths persist after all five LLMs are replaced with their current-generation successors.

cs.SE↗
arXiv2026

Smart Hiring Redefined: An Intelligent Recruitment Management Platform

Against the backdrop of deepening digital and intelligent transformation in human resource management, traditional recruitment models struggle to fully meet enterprises' growing demand for precise talent acquisition due to limited efficiency, high costs, and information asymmetry. As a vital tool for optimizing recruitment processes, reducing labor and time costs, and enhancing core competitiveness, intelligent recruitment management systems have become an indispensable component of modern organizational talent strategies. Compared with the labor intensive tasks of resume screening, candidate position matching, and interview coordination in traditional manual recruitment, intelligent recruitment systems significantly enhance the efficiency and accuracy of the hiring process through automation and data driven approaches. These systems enable rapid parsing of massive resume volumes, intelligent matching of candidates to positions, and automated scheduling of interview processes. This substantially reduces the workload on human resources departments while improving recruitment quality and response speed. This research leverages the Java technology framework to design and implement an intelligent recruitment management system tailored for campus recruitment scenarios. The system establishes a collaborative platform connecting students, enterprises, and administrators through information technology and intelligent solutions, offering comprehensive functionalities including job posting distribution, resume submission, candidate position matching, and process management. Guided by the vision of Smart Campus Recruitment, the project delivers a more convenient job seeking experience for students and provides enterprises with more efficient talent screening and recruitment management services, thereby driving high quality development in university enterprise collaboration.

cs.SE↗