Synthesizing Test Cases for Narrowing Specification Candidates

• URL: http://arxiv.org/abs/2511.19177v1
• Date: Mon, 24 Nov 2025 14:41:17 GMT
• Title: Synthesizing Test Cases for Narrowing Specification Candidates
• Authors: Alcino Cunha, Nuno Macedo,
• Abstract summary: Given a set of specifications, our technique generates a suite of test cases that, once classified by the user as desirable or not, narrows down the set of candidates to at most one specification.<n>Two alternative solver-based algorithms are proposed, one that generates a minimal test suite, and another that does not ensure minimality.
• Score: 1.2031796234206136
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper proposes a technique to help choose the best formal specification candidate among a set of alternatives. Given a set of specifications, our technique generates a suite of test cases that, once classified by the user as desirable or not, narrows down the set of candidates to at most one specification. Two alternative solver-based algorithms are proposed, one that generates a minimal test suite, and another that does not ensure minimality. Both algorithms were implemented in a prototype that can be used generate test suites to help choose among alternative Alloy specifications. Our evaluation of this prototype against a large set of problems showed that the optimal algorithm is efficient enough for many practical problems, and that the non-optimal algorithm can scale up to dozens of candidate specifications while still generating reasonably sized test suites.

Related papers

• Near Optimal Inference for the Best-Performing Algorithm [6.5268245109828005]
  We introduce a novel framework for the subset selection problem.<n>We provide both high confidence and finite-sample schemes that significantly improve upon currently known methods.
  arXiv  Detail & Related papers  (2025-08-07T09:08:06Z)
• Provable Scaling Laws for the Test-Time Compute of Large Language Models [84.00141420901038]
  We propose two algorithms that enjoy provable scaling laws for the test-time compute of large language models.<n>One is a two-stage knockout-style algorithm, where each candidate is evaluated by its average win rate against multiple opponents.<n>The other is a two-stage league-style algorithm, where each candidate is evaluated by its average win rate against multiple opponents.
  arXiv  Detail & Related papers  (2024-11-29T05:29:47Z)
• Stop Relying on No-Choice and Do not Repeat the Moves: Optimal, Efficient and Practical Algorithms for Assortment Optimization [38.57171985309975]
  We develop efficient algorithms for the problem of regret in assortment selection with emphPlackett Luce (PL) based user choices. Our methods are practical, provably optimal, and devoid of the aforementioned limitations of the existing methods.
  arXiv  Detail & Related papers  (2024-02-29T07:17:04Z)
• Dual-Directed Algorithm Design for Efficient Pure Exploration [9.728332815218181]
  We develop a new design principle for pure-exploration problems that extends the top-two approach beyond best-arm identification.<n>We prove that, when combined with Information-Directed Selection, top-two Thompson sampling attains optimality for best-arm identification.<n>We also produce optimal algorithms for thresholding bandits and $varepsilon$-best-arm identification.
  arXiv  Detail & Related papers  (2023-10-30T07:29:17Z)
• Machine Learning for Online Algorithm Selection under Censored Feedback [71.6879432974126]
  In online algorithm selection (OAS), instances of an algorithmic problem class are presented to an agent one after another, and the agent has to quickly select a presumably best algorithm from a fixed set of candidate algorithms. For decision problems such as satisfiability (SAT), quality typically refers to the algorithm's runtime. In this work, we revisit multi-armed bandit algorithms for OAS and discuss their capability of dealing with the problem. We adapt them towards runtime-oriented losses, allowing for partially censored data while keeping a space- and time-complexity independent of the time horizon.
  arXiv  Detail & Related papers  (2021-09-13T18:10:52Z)
• Algorithm Selection on a Meta Level [58.720142291102135]
  We introduce the problem of meta algorithm selection, which essentially asks for the best way to combine a given set of algorithm selectors. We present a general methodological framework for meta algorithm selection as well as several concrete learning methods as instantiations of this framework.
  arXiv  Detail & Related papers  (2021-07-20T11:23:21Z)
• Towards Meta-Algorithm Selection [78.13985819417974]
  Instance-specific algorithm selection (AS) deals with the automatic selection of an algorithm from a fixed set of candidates. We show that meta-algorithm-selection can indeed prove beneficial in some cases.
  arXiv  Detail & Related papers  (2020-11-17T17:27:33Z)
• Optimal 1-NN Prototypes for Pathological Geometries [13.70633147306388]
  Using prototype methods to reduce the size of training datasets can drastically reduce the computational cost of classification. We show that it is difficult to find the optimal prototypes for a given dataset, and algorithms are used instead. We propose an algorithm for finding nearly-optimal classifier prototypes in this setting, and use it to empirically validate the theoretical results.
  arXiv  Detail & Related papers  (2020-10-31T10:15:08Z)
• Run2Survive: A Decision-theoretic Approach to Algorithm Selection based on Survival Analysis [75.64261155172856]
  survival analysis (SA) naturally supports censored data and offers appropriate ways to use such data for learning distributional models of algorithm runtime. We leverage such models as a basis of a sophisticated decision-theoretic approach to algorithm selection, which we dub Run2Survive. In an extensive experimental study with the standard benchmark ASlib, our approach is shown to be highly competitive and in many cases even superior to state-of-the-art AS approaches.
  arXiv  Detail & Related papers  (2020-07-06T15:20:17Z)
• Extreme Algorithm Selection With Dyadic Feature Representation [78.13985819417974]
  We propose the setting of extreme algorithm selection (XAS) where we consider fixed sets of thousands of candidate algorithms. We assess the applicability of state-of-the-art AS techniques to the XAS setting and propose approaches leveraging a dyadic feature representation.
  arXiv  Detail & Related papers  (2020-01-29T09:40:58Z)

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.