Aug 2026· Proceedings of the 32nd ACM SIGKDD Conference on Knowledge Discovery and Data Mining V.2· pp. 7444-7455· 0 citations· 14 references
Abstract
Creating code specifications is a crucial measure to improve the trustworthiness of many industrial systems implemented in Rust with high security requirements. Because writing specifications requires highly specialized professionals and is time-consuming, the automatic generation of specifications, enabled by large language models (LLMs), has received increasing attention and shown promising results. However, these methods typically focus on partial specification generation (generating proofs after the contract is known) and on extracting dependencies between code modules using predefined relations. This is not suitable for real-world industrial systems where the goal is to generate complete specifications from scratch and where the complex dependencies between code modules are variable. To address this, we propose a multi-agent collaborative framework, StarVerus, to automate the verification of industrial Rust code. Specifically, StarVerus addresses the aforementioned limitations in two ways: 1) In the generation phase, it instructs the LLM to generate all specifications for a given code, and in the repair phase, it uses a cascaded two-stage process of contract alignment and proof repair to correct them; 2) In both the generation and repair phases, it utilizes a function call graph to adaptively obtain bidirectional contextual information (i.e., what it calls and what calls it) for each code module as an additional information source for the LLM. Furthermore, StarVerus introduces a planner-repairer-actor-rewriter multi-agent paradigm to further enhance the proof repair capabilities. Finally, the effectiveness of StarVerus is validated through experiments on benchmark datasets and deployment in a real operating system.
Results show that MAGen translates generic LLM competence into reproducible, automation-ready contract-and-test artifacts under a fixed validation protocol.
Lixue Liu, Wei Ke, Haiyang Chi et al.· Empirical Software Engineeri...· 0 citations
This work presents \textsc{SemaPLC}, a project-grounded and verification-gated agent harness assembled from conventional tools but governed by a strict completion rule, which raises the mean at every layer and most sharply at runtime.
Yanlun Tu, Huacan Wang, Ziyue Zhou et al.· 0 citations
Verification consumes the majority of modern chip design effort, yet the formal verification tools that provide mathematical guarantees of correctness remain expensive and restrictively licensed. While large language models (LLMs) have shown promise for hardware design, existing approaches to RTL repair validate their results through simulation - which exercises only a subset of inputs - or rely on commercial tools, and few combine formal proof with an entirely open-source toolchain. In this paper, we present a multi-agent pipeline that couples an LLM with an open-source formal backend (Yosys, SymbiYosys, and Z3) to repair RTL through counterexample-guided iteration: the framework generates formal properties, verifies the design, and feeds counterexamples back to the LLM until the design is proved correct by k-induction or an iteration budget is exhausted. Through an ALU case study, we show that the pipeline can detect and repair a real functional bug with a formal proof of correctness. Across a six-benchmark suite, one design is repaired reliably, and we characterize four distinct failure modes: bounded-cover vacuity, specification ambiguity, temporal-logic bugs, and multi-property pressure. We frame this work as a feasibility study with a detailed failure analysis, and additionally report a practical limitation of the Yosys bind directive relevant to the open-source formal verification community.
TestAgent is proposed, an LLM-based test generation approach that addresses the above limitations by emulating human testing practices via a multi-agent collaboration mechanism and equips TestAgent with a set of tool APIs that can be invoked dynamically in an on-demand and adaptive manner.
Quanjun Zhang, Ye Shang, Siqi Gu et al.· arXiv.org· 0 citations
This work proposes CodeSpec, a dual executable specification method for repository-level feature development that builds reliable functional chains from evidence pairing sub-requirement semantics with repository architectures, then compiles them into complementary architecture and behavior specifications that check chain completeness and correctness while preserving design-implementation consistency over long interactions.
Peiding Wang, Li Zhang, Fang Liu et al.· arXiv.org· 1 citation
Programmable Logic Controllers (PLCs) are central to industrial automation, yet their programming remains largely manual and time-consuming. While Large Language Models (LLMs) excel at general-purpose code generation, their use in industrial control is limited by tight coupling with physical hardware, constrained I/O signals, and strict safety requirements. We propose a novel approach to PLC code generation that takes as input structured lists of sensors and actuators from electrical CAD tools, together with the required control functionality. The task is formulated as generating machine-specific control functions grounded in available signals, ensuring physical implementability. The system is based on a single LLM adapted through multi-stage fine-tuning and enhanced with Retrieval-Augmented Generation (RAG). Experiments on error detection, code fixing, and code generation show that fine-tuning significantly improves performance. RAG provides strong gains in error detection and code generation, while offering limited benefit for code fixing, highlighting its task-dependent effectiveness.
Teresa Cacciapaglia, D. Ruffino, D. Naso et al.· International Conference on...· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
