Caruca: Effective and Efficient Specification Mining for Opaque Software Components

• URL: http://arxiv.org/abs/2510.14279v1
• Date: Thu, 16 Oct 2025 04:02:45 GMT
• Title: Caruca: Effective and Efficient Specification Mining for Opaque Software Components
• Abstract summary: Caruca is a system for automatic specification mining for opaque commands.<n>It generates correct specifications for all but one case.<n>It is currently powering the full specifications for a state-of-the-art static analysis tool.
• Score: 2.7058710173622544
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: A wealth of state-of-the-art systems demonstrate impressive improvements in performance, security, and reliability on programs composed of opaque components, such as Unix shell commands. To reason about commands, these systems require partial specifications. However, creating such specifications is a manual, laborious, and error-prone process, limiting the practicality of these systems. This paper presents Caruca, a system for automatic specification mining for opaque commands. To overcome the challenge of language diversity across commands, Caruca first instruments a large language model to translate a command's user-facing documentation into a structured invocation syntax. Using this representation, Caruca explores the space of syntactically valid command invocations and execution environments. Caruca concretely executes each command-environment pair, interposing at the system-call and filesystem level to extract key command properties such as parallelizability and filesystem pre- and post-conditions. These properties can be exported in multiple specification formats and are immediately usable by existing systems. Applying Caruca across 60 GNU Coreutils, POSIX, and third-party commands across several specification-dependent systems shows that Caruca generates correct specifications for all but one case, completely eliminating manual effort from the process and currently powering the full specifications for a state-of-the-art static analysis tool.

Related papers

• Youtu-Parsing: Perception, Structuring and Recognition via High-Parallelism Decoding [35.429403152845836]
  Youtu-Parsing is an efficient and versatile document parsing model designed for high-performance content extraction.<n>The model exhibits strong robustness when handling rare characters, multilingual text, and handwritten content.<n>Youtu-Parsing achieves state-of-the-art (SOTA) performance on the OmniDocBench and olmOCR-bench benchmarks.
  arXiv  Detail & Related papers  (2026-01-28T09:37:13Z)
• Sharpen the Spec, Cut the Code: A Case for Generative File System with SYSSPEC [6.536447932095715]
  This paper introduces SYSSPEC, a framework for developing generative file systems.<n>Instead of imprecise prompts, SYSSPEC employs a multi-part specification that accurately describes a file system's functionality.<n>To manage evolution, we develop a DAG-structured patch that operates on the specification itself.
  arXiv  Detail & Related papers  (2025-12-15T07:15:01Z)
• WGRAMMAR: Leverage Prior Knowledge to Accelerate Structured Decoding [58.1177179119881]
  We introduce wgrammar, a lightweight decoding engine that integrates domain-aware simplification, constraint decomposition, and mask caching.<n> wgrammar achieves up to 250x speedup over existing systems.
  arXiv  Detail & Related papers  (2025-07-22T17:13:47Z)
• Classifier-Guided Captioning Across Modalities [69.75111271002137]
  We introduce a method to adapt captioning networks to the semantics of alternative settings, such as capturing audibility in audio captioning.<n>Our framework consists of two main components: (i) a frozen captioning system incorporating a language model (LM), and (ii) a text classifier that guides the captioning system.<n> Notably, when combined with an existing zero-shot audio captioning system, our framework improves its quality and sets state-of-the-art performance in zero-shot audio captioning.
  arXiv  Detail & Related papers  (2025-01-03T18:09:26Z)
• From Commands to Prompts: LLM-based Semantic File System for AIOS [46.29019415676847]
  We propose an LLM-based semantic file system ( LSFS) for prompt-driven file management.<n>Unlike conventional approaches, LSFS incorporates LLMs to enable users or agents to interact with files through natural language prompts.<n>Our experiments show that LSFS offers significant improvements over traditional file systems in terms of user convenience, the diversity of supported functions, and the accuracy and efficiency of file operations.
  arXiv  Detail & Related papers  (2024-09-23T08:39:16Z)
• VideoGUI: A Benchmark for GUI Automation from Instructional Videos [78.97292966276706]
  VideoGUI is a novel multi-modal benchmark designed to evaluate GUI assistants on visual-centric GUI tasks. Sourced from high-quality web instructional videos, our benchmark focuses on tasks involving professional and novel software. Our evaluation reveals that even the SoTA large multimodal model GPT4o performs poorly on visual-centric GUI tasks.
  arXiv  Detail & Related papers  (2024-06-14T17:59:08Z)
• ControlCap: Controllable Region-level Captioning [57.57406480228619]
  Region-level captioning is challenged by the caption degeneration issue. Pre-trained multimodal models tend to predict the most frequent captions but miss the less frequent ones. We propose a controllable region-level captioning approach, which introduces control words to a multimodal model.
  arXiv  Detail & Related papers  (2024-01-31T15:15:41Z)
• InstructSeq: Unifying Vision Tasks with Instruction-conditioned Multi-modal Sequence Generation [59.24938416319019]
  InstructSeq is an instruction-conditioned multi-modal modeling framework. It unifies diverse vision tasks through flexible natural language control and handling of both visual and textual data.
  arXiv  Detail & Related papers  (2023-11-30T18:59:51Z)
• Large Language Models Based Automatic Synthesis of Software Specifications [3.081650600579376]
  SpecSyn is a framework that automatically synthesizes software specifications from natural language sources. Our approach formulates software specification synthesis as a sequence-to-sequence learning problem.
  arXiv  Detail & Related papers  (2023-04-18T01:22:44Z)
• Automatic Extraction of Rules Governing Morphological Agreement [103.78033184221373]
  We develop an automated framework for extracting a first-pass grammatical specification from raw text. We focus on extracting rules describing agreement, a morphosyntactic phenomenon at the core of the grammars of many of the world's languages. We apply our framework to all languages included in the Universal Dependencies project, with promising results.
  arXiv  Detail & Related papers  (2020-10-02T18:31:45Z)

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.