Skip to content

From Resource Flow to Executable Tests: Petri-Net-Guided LLM Test Generation for Concurrent Stateful Rust APIs

Jul 2026 · arXiv.org · Vol abs/2607.21530 · 0 citations · 9 references
Computer Science

TL;DR

A Petri-net-guided methodology for test generation over concurrent stateful Rust APIs that represents API resources, lifecycle conditions, and causal dependencies as colored tokens and transitions; derives legal deep-state, near-legal, and partial-order concurrent scenarios; and uses them as a constrained intermediate representation for LLM-based code synthesis.

Abstract

Concurrent stateful library APIs expose behavior through evolving resource ownership, lifecycle states, and competing interleavings. Large language models can synthesize executable Rust tests, but their outputs often violate API preconditions, remain shallow, or reduce concurrency to accidental sequential traces. Conversely, model-based and systematic testing techniques provide semantic control but commonly require substantial handwritten code to turn abstract scenarios into executable tests. This paper addresses the gap between formal scenario design and low-cost test concretization. We present a Petri-net-guided methodology for test generation over concurrent stateful Rust APIs. The method represents API resources, lifecycle conditions, and causal dependencies as colored tokens and transitions; derives legal deep-state, near-legal, and partial-order concurrent scenarios; and uses these scenarios as a constrained intermediate representation for LLM-based code synthesis. A local-faithfulness contract and structural repair loop preserve the modeled intent during concretization, while Petri-guided schedule shaping prioritizes high-conflict concurrency skeletons for systematic exploration. A layered semantic oracle then distinguishes synthesis failures from violations of the target API's expected behavior.

View source

Similar papers

Preprint Jul 2026

Teaching Code LLMs to Reason with Intermediate Formal Specifications

This paper introduces SpecCoder, a verification-guided CodeLLM training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces, and improves checkpoint-specification quality over base CodeLLMs, and introduces HumanExec, a benchmark built from r...

Minh Le-Anh, Cuong Chi Le, Tien N. Nguyen · 0 citations
Book Open access Aug 2026

IntentP4: Bridging P4 Temporal Specifications and Executable Network Tests

IntentP4 is presented, a formal-methods-aided pipeline that translates an operator's natural-language intent into a P4LTL specification and then into a replayable multi-packet test case, grounded throughout in compiler artifacts via a tool-queryable ProgramContext and gated by deterministic per-stage validators.

Ruonan Feng, Mingming Zhang, Yu Jiang et al. · 0 citations
Book Aug 2026

Can Formal Specifications Be Synthesized from Tests Alone?

This approach uses LLMs to infer candidate specifications solely from test code and dynamic execution traces: the LLM observes only the program interface, selected inputs, and corresponding outputs or state changes, while the implementation internals remain hidden.

Tian-Hai Liu, Maximilian Müller, Tobias Hey et al. · 0 citations
Jul 2026

InstantInfer: Enabling Fast LLM Cold Start with Communicating Finite Automata

This work proposes the Communicating Finite Automata (CFA) abstraction to systematically analyze cross-component optimization opportunities, and designs a programming framework to enable CFA-based component program refactoring that preserves the original sequential program structure while enabling safe concurrent compo...

Yitao Yuan, Yongchao He, Shaoke Fang et al. · 0 citations
Conference Open access Sep 2026

QiMeng-VPID: Verification-Grounded Port-Level Iterative Decomposition for Complex Verilog Generation

This work proposes VPID, a multi-agent framework for generating complex Verilog that achieves monotonic functional improvement and introduces an experience-guided refinement strategy that distills historical waveform mismatches into constraints, guiding the targeted debugging for the unverified ports.

Hong-Guang Wang, Jiaming Guo, Rui Zhang et al. · 0 citations
Preprint Aug 2026

REST API Testing with Verified LLM-Inferred Dependencies and Response-Driven Refinement

APIPilot first derives candidate producer-consumer dependencies from OpenAPI specifications using structural heuristics and LLM-based semantic reasoning and validates them through concrete API executions before using them for test generation, outperforming both LLM-based and traditional REST API testing baselines.

Tuong Nguyen, Thanh Nguyen, Huy Nguyen et al. · 0 citations

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.