FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs

• URL: http://arxiv.org/abs/2502.15217v1
• Date: Fri, 21 Feb 2025 05:20:04 GMT
• Title: FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs
• Authors: Madhurima Chakraborty, Peter Pirkelbauer, Qing Yi,
• Abstract summary: FormalSpecCpp is a dataset designed to fill the gap in standardized benchmarks for verifying formal specifications in C++ programs.<n>It provides a structured benchmark for evaluating specification inference tools and testing theaccuracy of generated specifications.
• Score: 0.3277163122167433
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: FormalSpecCpp is a dataset designed to fill the gap in standardized benchmarks for verifying formal specifications in C++ programs. To the best of our knowledge, this is the first comprehensive collection of C++ programs with well-defined preconditions and postconditions. It provides a structured benchmark for evaluating specification inference tools and testing theaccuracy of generated specifications. Researchers and developers can use this dataset to benchmark specification inference tools,fine-tune Large Language Models (LLMs) for automated specification generation, and analyze the role of formal specifications in improving program verification and automated testing. By making this dataset publicly available, we aim to advance research in program verification, specification inference, and AI-assisted software development. The dataset and the code are available at https://github.com/MadhuNimmo/FormalSpecCpp.

Related papers

• Do AI models help produce verified bug fixes? [62.985237003585674]
  Large Language Models are used to produce corrections to software bugs.<n>This paper investigates how programmers use Large Language Models to complement their own skills.<n>The results are a first step towards a proper role for AI and LLMs in providing guaranteed-correct fixes to program bugs.
  arXiv  Detail & Related papers  (2025-07-21T17:30:16Z)
• Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
  VERIFAI1 aims to investigate automated and semi-automated approaches to bridge this gap.<n>This position paper presents a preliminary synthesis of relevant literature to identify recurring challenges and prospective research directions.
  arXiv  Detail & Related papers  (2025-07-18T19:15:50Z)
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [84.30534714651093]
  We present an innovative APR tool for Dafny, a verification-aware programming language.<n>We localize faults through a series of steps, which include using Hoare Logic to determine the state of each statement within the program.<n>We evaluate our approach using DafnyBench, a benchmark of real-world Dafny programs.
  arXiv  Detail & Related papers  (2025-07-04T15:36:12Z)
• OpenCodeInstruct: A Large-scale Instruction Tuning Dataset for Code LLMs [62.68905180014956]
  We introduce OpenCodeInstruct, the largest open-access instruction tuning dataset, comprising 5 million diverse samples. Each sample includes a programming question, solution, test cases, execution feedback, and LLM-generated quality assessments. We fine-tune various base models, including LLaMA and Qwen, across multiple scales (1B+, 3B+, and 7B+) using our dataset.
  arXiv  Detail & Related papers  (2025-04-05T02:52:16Z)
• ClassInvGen: Class Invariant Synthesis using Large Language Models [11.374431160444676]
  ClassInvGen is a method for co-generating executable class invariants and test inputs. We show that ClassInvGen outperforms a pure LLM-based technique to generate specifications (from code) We also demonstrate its applicability to real-world code by performing a case study on several classes within a widely used and high-integrity C++.
  arXiv  Detail & Related papers  (2025-02-26T08:10:57Z)
• CPP-UT-Bench: Can LLMs Write Complex Unit Tests in C++? [0.4915744683251149]
  CPP-UT-Bench is a benchmark dataset to measure C++ unit test generation capability of a large language model (LLM) The dataset includes 2,653 code, unit test pairs drawn from 14 different opensource C++s.
  arXiv  Detail & Related papers  (2024-12-03T18:35:24Z)
• AutoBencher: Towards Declarative Benchmark Construction [74.54640925146289]
  We use AutoBencher to create datasets for math, multilinguality, knowledge, and safety. The scalability of AutoBencher allows it to test fine-grained categories knowledge, creating datasets that elicit 22% more model errors (i.e., difficulty) than existing benchmarks.
  arXiv  Detail & Related papers  (2024-07-11T10:03:47Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  We propose a metric for evaluating the quality of specifications for verification-aware languages. We show that our metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark. We also outline formal verification challenges that need to be addressed to apply the technique more widely.
  arXiv  Detail & Related papers  (2024-06-14T06:52:08Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpec is an automated approach to synthesize specifications for automated program verification. It overcomes the shortcomings of existing work in specification versatility, synthesizing satisfiable and adequate specifications for full proof. It can be successfully applied to verify the programs in a real-world X509-parser project.
  arXiv  Detail & Related papers  (2024-03-31T18:15:49Z)
• SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
  SpecGen is a novel technique for formal program specification generation based on Large Language Models.<n>We evaluate SpecGen on two datasets, including the SV-COMP 279 benchmark and a manually constructed dataset.
  arXiv  Detail & Related papers  (2024-01-16T20:13:50Z)
• Instruct and Extract: Instruction Tuning for On-Demand Information Extraction [86.29491354355356]
  On-Demand Information Extraction aims to fulfill the personalized demands of real-world users. We present a benchmark named InstructIE, inclusive of both automatically generated training data, as well as the human-annotated test set. Building on InstructIE, we further develop an On-Demand Information Extractor, ODIE.
  arXiv  Detail & Related papers  (2023-10-24T17:54:25Z)
• Python Code Generation by Asking Clarification Questions [57.63906360576212]
  In this work, we introduce a novel and more realistic setup for this task. We hypothesize that the under-specification of a natural language description can be resolved by asking clarification questions. We collect and introduce a new dataset named CodeClarQA containing pairs of natural language descriptions and code with created synthetic clarification questions and answers.
  arXiv  Detail & Related papers  (2022-12-19T22:08:36Z)
• CodeExp: Explanatory Code Document Generation [94.43677536210465]
  Existing code-to-text generation models produce only high-level summaries of code. We conduct a human study to identify the criteria for high-quality explanatory docstring for code. We present a multi-stage fine-tuning strategy and baseline models for the task.
  arXiv  Detail & Related papers  (2022-11-25T18:05:44Z)
• GEMv2: Multilingual NLG Benchmarking in a Single Line of Code [161.1761414080574]
  Generation, Evaluation, and Metrics Benchmark introduces a modular infrastructure for dataset, model, and metric developers. GEMv2 supports 40 documented datasets in 51 languages. Models for all datasets can be evaluated online and our interactive data card creation and rendering tools make it easier to add new datasets to the living benchmark.
  arXiv  Detail & Related papers  (2022-06-22T17:52:30Z)

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.