Automatic Program Instrumentation for Automatic Verification (Extended Technical Report)

• URL: http://arxiv.org/abs/2306.00004v1
• Date: Fri, 26 May 2023 14:55:35 GMT
• Title: Automatic Program Instrumentation for Automatic Verification (Extended Technical Report)
• Authors: Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidstr\"om, Philipp R\"ummer
• Abstract summary: 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.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about its correctness instead. In this paper, we propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We formalise array aggregation operations as monoid homomorphisms. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.

Related papers

• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  We propose a metric for evaluating the quality of specifications for verification-aware languages. We show that our metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark. We also outline formal verification challenges that need to be addressed to apply the technique more widely.
  arXiv  Detail & Related papers  (2024-06-14T06:52:08Z)
• Prompt Optimization with EASE? Efficient Ordering-aware Automated Selection of Exemplars [66.823588073584]
  Large language models (LLMs) have shown impressive capabilities in real-world applications. The quality of these exemplars in the prompt greatly impacts performance. Existing methods fail to adequately account for the impact of exemplar ordering on the performance.
  arXiv  Detail & Related papers  (2024-05-25T08:23:05Z)
• Bisimulation Learning [55.859538562698496]
  We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpec is an automated approach to synthesize specifications for automated program verification. It overcomes the shortcomings of existing work in specification versatility, synthesizing satisfiable and adequate specifications for full proof. It can be successfully applied to verify the programs in a real-world X509-parser project.
  arXiv  Detail & Related papers  (2024-03-31T18:15:49Z)
• Quantitative Assurance and Synthesis of Controllers from Activity Diagrams [4.419843514606336]
  Probabilistic model checking is a widely used formal verification technique to automatically verify qualitative and quantitative properties. This makes it not accessible for researchers and engineers who may not have the required knowledge. We propose a comprehensive verification framework for ADs, including a new profile for probability time, quality annotations, a semantics interpretation of ADs in three Markov models, and a set of transformation rules from activity diagrams to the PRISM language. Most importantly, we developed algorithms for transformation and implemented them in a tool, called QASCAD, using model-based techniques, for fully automated verification.
  arXiv  Detail & Related papers  (2024-02-29T22:40:39Z)
• 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)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  We provide a framework to encode system specifications and define corresponding certificates. We present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
  arXiv  Detail & Related papers  (2023-09-12T09:37:26Z)
• On the Limits of Evaluating Embodied Agent Model Generalization Using Validation Sets [101.28658250723804]
  This paper experiments with augmenting a transformer model with modules that effectively utilize a wider field of view and learn to choose whether the next step requires a navigation or manipulation action. We observe that the proposed modules resulted in improved, and in fact state-of-the-art performance on an unseen validation set of a popular benchmark dataset, ALFRED. We highlight this result as we believe it may be a wider phenomenon in machine learning tasks but primarily noticeable only in benchmarks that limit evaluations on test splits.
  arXiv  Detail & Related papers  (2022-05-18T23:52:21Z)
• Automated Aggregator -- Rewriting with the Counting Aggregate [0.0]
  We present an automated rewriting system that produces a family of equivalent programs with complementary performance. We propose the system's use in automated answer set programming solver selection tools.
  arXiv  Detail & Related papers  (2020-09-22T00:48:33Z)
• Generating Fact Checking Explanations [52.879658637466605]
  A crucial piece of the puzzle that is still missing is to understand how to automate the most elaborate part of the process. This paper provides the first study of how these explanations can be generated automatically based on available claim context. Our results indicate that optimising both objectives at the same time, rather than training them separately, improves the performance of a fact checking system.
  arXiv  Detail & Related papers  (2020-04-13T05:23:25Z)

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.