Tunable Automation in Automated Program Verification

• URL: http://arxiv.org/abs/2512.03926v1
• Date: Wed, 03 Dec 2025 16:27:01 GMT
• Title: Tunable Automation in Automated Program Verification
• Authors: Alexander Y. Bai, Chris Hawblitzel, Andrea Lattuada,
• Abstract summary: SMT-based verification tools face a tension between automation and performance when dealing with quantifier instantiation.<n>We present a mechanism that enables fine-grained control over the availability of quantified facts in verification contexts.<n>We implement our techniques in Verus, a Rust-based verification tool, and evaluate them on multiple openly availables.
• Score: 42.02726718338287
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Automated verification tools based on SMT solvers have made significant progress in verifying complex software systems. However, these tools face a fundamental tension between automation and performance when dealing with quantifier instantiation -- the primary source of incompleteness and verification slowdown in SMT-based verifiers. Tools choose between aggressive quantifier instantiation that provides more automation but longer verification times, or conservative instantiation that responds quickly but may require more manual proof hints. We present a mechanism that enables fine-grained control over the availability of quantified facts in verification contexts, allowing developers to selectively tune the level of automation. Our approach lets library authors provide different pre-defined automation levels while giving end-users the ability to further customize quantifier availability at the module, function, or proof context level. We implement our techniques in Verus, a Rust-based verification tool, and evaluate them on multiple openly available codebases. Our empirical analysis demonstrates the automation-performance tradeoff and that selective quantifier management enables developers to select the appropriate level of automation in different contexts.

Related papers

• Auditable DevOps Automation via VSM and GQM [0.0]
  This paper presents textitVSM--GQM--DevOps,' a unified framework that visualizes the end-to-end delivery system and quantify delays, rework, and handoffs.<n>The framework operationalizes traceability from observed waste to goal-aligned questions, metrics, and automation candidates, and provides a defensible prioritization approach.
  arXiv  Detail & Related papers  (2026-01-07T04:36:24Z)
• AutoEDA: Enabling EDA Flow Automation through Microservice-Based LLM Agents [15.41283323575065]
  AutoEDA is a framework for EDA automation that leverages paralleled learning through the Model Context Protocol (MCP) specific for standardized and scalable natural language experience.<n>Results from experiments show improvements in automation accuracy and efficiency, as well as script quality when compared to existing methods.
  arXiv  Detail & Related papers  (2025-08-01T18:23:57Z)
• AutoAct: Automatic Agent Learning from Scratch for QA via Self-Planning [54.47116888545878]
  AutoAct is an automatic agent learning framework for QA. It does not rely on large-scale annotated data and synthetic planning trajectories from closed-source models.
  arXiv  Detail & Related papers  (2024-01-10T16:57:24Z)
• TaskBench: Benchmarking Large Language Models for Task Automation [82.2932794189585]
  We introduce TaskBench, a framework to evaluate the capability of large language models (LLMs) in task automation. Specifically, task decomposition, tool selection, and parameter prediction are assessed. Our approach combines automated construction with rigorous human verification, ensuring high consistency with human evaluation.
  arXiv  Detail & Related papers  (2023-11-30T18:02:44Z)
• Lemur: Integrating Large Language Models in Automated Program Verification [10.221822902660458]
  We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We instantiate the calculus as a sound automated verification procedure and demonstrate practical improvements on a set of synthetic and competition benchmarks.
  arXiv  Detail & Related papers  (2023-10-07T16:44:53Z)
• The Devil is in the Errors: Leveraging Large Language Models for Fine-grained Machine Translation Evaluation [93.01964988474755]
  AutoMQM is a prompting technique which asks large language models to identify and categorize errors in translations. We study the impact of labeled data through in-context learning and finetuning. We then evaluate AutoMQM with PaLM-2 models, and we find that it improves performance compared to just prompting for scores.
  arXiv  Detail & Related papers  (2023-08-14T17:17:21Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  In deductive verification and software model checking, dealing with certain specification language constructs can be problematic. We propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation.
  arXiv  Detail & Related papers  (2023-05-26T14:55:35Z)
• Unsupervised Automata Learning via Discrete Optimization [4.5726613073750135]
  We propose a framework for learning a deterministic finite automaton (DFA) from a given multi-set of unlabeled words.<n>We show that this problem is computationally hard and develop three learning algorithms based on constraint optimization.<n>We introduce novel regularization schemes for our optimization problems that improve the overall interpretability of our DFAs.
  arXiv  Detail & Related papers  (2023-03-24T16:19:15Z)
• Automated Machine Learning Techniques for Data Streams [91.3755431537592]
  This paper surveys the state-of-the-art open-source AutoML tools, applies them to data collected from streams, and measures how their performance changes over time. The results show that off-the-shelf AutoML tools can provide satisfactory results but in the presence of concept drift, detection or adaptation techniques have to be applied to maintain the predictive accuracy over time.
  arXiv  Detail & Related papers  (2021-06-14T11:42:46Z)
• Induction and Exploitation of Subgoal Automata for Reinforcement Learning [75.55324974788475]
  We present ISA, an approach for learning and exploiting subgoals in episodic reinforcement learning (RL) tasks. ISA interleaves reinforcement learning with the induction of a subgoal automaton, an automaton whose edges are labeled by the task's subgoals. A subgoal automaton also consists of two special states: a state indicating the successful completion of the task, and a state indicating that the task has finished without succeeding.
  arXiv  Detail & Related papers  (2020-09-08T16:42:55Z)

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.