Systematic API Testing Through Model Checking and Executable Contracts

• URL: http://arxiv.org/abs/2604.08633v1
• Date: Thu, 09 Apr 2026 17:00:42 GMT
• Title: Systematic API Testing Through Model Checking and Executable Contracts
• Abstract summary: We introduce IcePick, a framework that achieves systematic state-space coverage for API testing by leveraging model checking.<n>IcePick uses TLA+ to formally model API state evolution, employs the TLC model checker to exhaustively explore reachable states, and generates test sequences that provably cover the behavioural model.<n>To address oracle limitations beyond HTTP status codes, we propose Glacier, a first-order logic contract language that enriches API specifications with executable semantic contracts.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated black-box testing of APIs typically relies on interface specifications that define available operations and data schemas, but offer limited or no behavioural semantics. This semantic gap amplifies the test-oracle problem and limits the generation of effective, stateful call sequences. We introduce IcePick, a framework that achieves systematic state-space coverage for API testing by leveraging model checking. IcePick uses TLA+ to formally model API state evolution, employs the TLC model checker to exhaustively explore reachable states, and generates test sequences that provably cover the behavioural model. To mitigate state-space explosion and improve sequence extraction, we introduce a coverage-guided breadth-first traversal of the TLC state-space graph. To address oracle limitations beyond HTTP status codes, we propose Glacier, a first-order logic contract language that enriches API specifications with executable semantic contracts, enabling automated behavioural verification during test execution. We evaluate IcePick on EvoMaster Benchmark systems, demonstrating that model-checking-guided exploration achieves complete state coverage and reveals faults in multi-operation interactions. We also analyse scalability to characterise practical limits and applicability requirements. Overall, IcePick provides reproducible test suites with strong coverage guarantees for critical API-based systems.

Related papers

• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
  arXiv  Detail & Related papers  (2026-08-04T13:01:30Z)
• From Resource Flow to Executable Tests: Petri-Net-Guided LLM Test Generation for Concurrent Stateful Rust APIs [5.064868362565062]
  Concurrent stateful library APIs expose behavior through evolving resource ownership, lifecycle states, and competing interleavings.<n>Large language models can synthesize executable Rust tests, but their outputs often violate API preconditions, remain shallow, or reduce to accidental traces.<n>This paper addresses the gap between formal scenario design and low-cost test concretization.
  arXiv  Detail & Related papers  (2026-07-23T17:15:53Z)
• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  We present PhyAgentOS, a foundation delivering scheduling, verification, memory, benchmarking, and safety as system-level services.<n>Its Session-Centered treats a session, not an action, as the minimum unit of scheduling, compatibility, supervised execution, evidence collection, and acceptance.<n>SessionVerifier distinguishes execution termination from semantic task completion via evidence-grounded verdicts of success, failure, or replan.<n> Benchmarking reuses the deployment session and verification path, so results trace to real execution.
  arXiv  Detail & Related papers  (2026-07-18T04:46:53Z)
• What to Test Next: Interpretable Coverage Gap Discovery in Driving VLMs [52.50210189669399]
  Driving vision-language models (VLMs) must accurately understand scenes across diverse conditions defined by Operational Design Domains (ODDs)<n>We propose SliceScorer, a deterministic scoring rule for missing-slice recommendation.<n>We show that SliceNav surfaces high-risk coverage gaps more effectively than prior slice-discovery methods.
  arXiv  Detail & Related papers  (2026-06-01T03:18:01Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Combining Static and Dynamic Approaches for Mining and Testing Constraints for RESTful API Testing [10.13889120511225]
  We propose to combine a novel static analysis approach (in which the constraints for API response bodies are mined from API specifications) with the dynamic approach.<n>We leverage large language models (LLMs) to comprehend the API specifications, mine constraints for response bodies, and generate test cases.<n>We also use its generated test cases to detect 21 mismatches between the API specification and actual response data for 8 real-world APIs.
  arXiv  Detail & Related papers  (2025-04-24T06:28:18Z)
• Test Amplification for REST APIs via Single and Multi-Agent LLM Systems [1.6499388997661122]
  We investigate the use of large language model (LLM) systems, both single-agent and multi-agent setups, for amplifying existing REST API test suites.<n>We present a comparative evaluation of the two approaches across several dimensions, including test coverage, bug detection effectiveness, and practical considerations such as computational cost and energy usage.
  arXiv  Detail & Related papers  (2025-04-10T20:19:50Z)
• Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [71.7892165868749]
  Commercial Large Language Model (LLM) APIs create a fundamental trust problem.<n>Users pay for specific models but have no guarantee that providers deliver them faithfully.<n>We formalize this model substitution problem and evaluate detection methods under realistic adversarial conditions.<n>We propose and evaluate the use of Trusted Execution Environments (TEEs) as one practical and robust solution.
  arXiv  Detail & Related papers  (2025-04-07T03:57:41Z)
• Utilizing API Response for Test Refinement [2.8002188463519944]
  This paper proposes a dynamic test refinement approach that leverages the response message.<n>Using an intelligent agent, the approach adds constraints to the API specification that are further used to generate a test scenario.<n>The proposed approach led to a decrease in the number of 4xx responses, taking a step closer to generating more realistic test cases.
  arXiv  Detail & Related papers  (2025-01-30T05:26:32Z)
• LlamaRestTest: Effective REST API Testing with Small Language Models [50.058600784556816]
  We present LlamaRestTest, a novel approach that employs two custom Large Language Models (LLMs) to generate realistic test inputs.<n>We evaluate it against several state-of-the-art REST API testing tools, including RESTGPT, a GPT-powered specification-enhancement tool.<n>Our study shows that small language models can perform as well as, or better than, large language models in REST API testing.
  arXiv  Detail & Related papers  (2025-01-15T05:51:20Z)
• DeepREST: Automated Test Case Generation for REST APIs Exploiting Deep Reinforcement Learning [5.756036843502232]
  This paper introduces DeepREST, a novel black-box approach for automatically testing REST APIs. It leverages deep reinforcement learning to uncover implicit API constraints, that is, constraints hidden from API documentation. Our empirical validation suggests that the proposed approach is very effective in achieving high test coverage and fault detection.
  arXiv  Detail & Related papers  (2024-08-16T08:03:55Z)
• FANTAstic SEquences and Where to Find Them: Faithful and Efficient API Call Generation through State-tracked Constrained Decoding and Reranking [57.53742155914176]
  API call generation is the cornerstone of large language models' tool-using ability. Existing supervised and in-context learning approaches suffer from high training costs, poor data efficiency, and generated API calls that can be unfaithful to the API documentation and the user's request. We propose an output-side optimization approach called FANTASE to address these limitations.
  arXiv  Detail & Related papers  (2024-07-18T23:44:02Z)
• KAT: Dependency-aware Automated API Testing with Large Language Models [1.7264233311359707]
  KAT (Katalon API Testing) is a novel AI-driven approach that autonomously generates test cases to validate APIs. Our evaluation of KAT using 12 real-world services shows that it can improve validation coverage, detect more undocumented status codes, and reduce false positives in these services.
  arXiv  Detail & Related papers  (2024-07-14T14:48:18Z)
• Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
  AuditAI bridges the gap between interpretable formal verification and scalability. We show how AuditAI allows us to obtain controlled variations for verification and certified training while addressing the limitations of verifying using only pixel-space perturbations.
  arXiv  Detail & Related papers  (2021-09-25T22:53:24Z)
• Complex Event Forecasting with Prediction Suffix Trees: Extended Technical Report [70.7321040534471]
  Complex Event Recognition (CER) systems have become popular in the past two decades due to their ability to "instantly" detect patterns on real-time streams of events. There is a lack of methods for forecasting when a pattern might occur before such an occurrence is actually detected by a CER engine. We present a formal framework that attempts to address the issue of Complex Event Forecasting.
  arXiv  Detail & Related papers  (2021-09-01T09:52:31Z)

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.