Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification

• URL: http://arxiv.org/abs/2208.05046v2
• Date: Tue, 12 Mar 2024 21:38:30 GMT
• Title: Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
• Authors: Dirk Beyer, Nian-Ze Lee, and Philipp Wendler
• Abstract summary: A formalverification algorithm was originally devised to verify safety properties of finite-state transition systems. Although 20 years old, the algorithm is still state-of-the-art in hardware model checking. Our contribution is to close this significant, two decades old gap in knowledge by adopting the algorithm to software verification.
• Score: 3.9403985159394144
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The article "Interpolation and SAT-Based Model Checking" (McMillan, 2003) describes a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. It derives interpolants from unsatisfiable BMC queries and collects them to construct an overapproximation of the set of reachable states. Although 20 years old, the algorithm is still state-of-the-art in hardware model checking. Unlike other formal-verification algorithms, such as k-induction or PDR, which have been extended to handle infinite-state systems and investigated for program analysis, McMillan's interpolation-based model-checking algorithm from 2003 has not been used to verify programs so far. Our contribution is to close this significant, two decades old gap in knowledge by adopting the algorithm to software verification. We implemented it in the verification framework CPAchecker and evaluated the implementation against other state-of-the-art software-verification techniques on the largest publicly available benchmark suite of C safety-verification tasks. The evaluation demonstrates that McMillan's interpolation-based model-checking algorithm from 2003 is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results are important for the area of software verification, because researchers and developers now have one more approach to choose from.

Related papers

• Formally Verified Approximate Policy Iteration [11.602089225841633]
  We show how the formalized algorithm can be refined to an executable, verified implementation. The implementation is evaluated on benchmark problems to show its practicability. As part of the refinement, we develop verified software to certify Linear Programming solutions.
  arXiv  Detail & Related papers  (2024-06-11T15:07:08Z)
• 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)
• Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version) [4.309079367183251]
  We propose an augmented-based verification algorithm that injects external invariants into model checking. We found that injecting invariants reduces the number of queries needed to prove safety properties and improves the run-time efficiency.
  arXiv  Detail & Related papers  (2024-03-12T17:02:53Z)
• An algorithm for clustering with confidence-based must-link and cannot-link constraints [0.0]
  We introduce the PCCC (Pairwise-Confidence-Constraints-Clustering) algorithm. The PCCC algorithm iteratively assigns objects to clusters while accounting for the information provided on the pairs of objects. Unlike existing algorithms, our algorithm scales to large-scale instances with up to 60,000 objects, 100 clusters, and millions of cannot-link constraints.
  arXiv  Detail & Related papers  (2022-12-29T19:21:33Z)
• Benchmarking Quality-Dependent and Cost-Sensitive Score-Level Multimodal Biometric Fusion Algorithms [58.156733807470395]
  This paper reports a benchmarking study carried out within the framework of the BioSecure DS2 (Access Control) evaluation campaign. The campaign targeted the application of physical access control in a medium-size establishment with some 500 persons. To the best of our knowledge, this is the first attempt to benchmark quality-based multimodal fusion algorithms.
  arXiv  Detail & Related papers  (2021-11-17T13:39:48Z)
• 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)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
  arXiv  Detail & Related papers  (2021-03-18T20:22:50Z)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  We develop and evaluate a novel symbolic verification framework using incremental bounded model checking (BMC), satisfiability modulo theories (SMT), and invariant inference. Our approach was able to verify and produce examples for 85.8% of 21 test cases considering different input images, and 100% of the properties related to covering methods.
  arXiv  Detail & Related papers  (2020-12-21T10:03:44Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  We investigate the problem of best-policy identification in discounted Markov Decision (MDPs) when the learner has access to a generative model. The advantages of state-of-the-art algorithms are discussed and illustrated.
  arXiv  Detail & Related papers  (2020-09-28T15:22:24Z)
• A Constraint-Based Algorithm for the Structural Learning of Continuous-Time Bayesian Networks [70.88503833248159]
  We propose the first constraint-based algorithm for learning the structure of continuous-time Bayesian networks. We discuss the different statistical tests and the underlying hypotheses used by our proposal to establish conditional independence.
  arXiv  Detail & Related papers  (2020-07-07T07:34:09Z)
• Verification and Validation of Convex Optimization Algorithms for Model Predictive Control [1.5322124183968633]
  This article discusses the formal verification of the Ellipsoid method, a convex optimization algorithm, and its code implementation. The applicability and limitations of those code properties and proofs are presented as well. Modifications to the algorithm are presented which can be used to control its numerical stability.
  arXiv  Detail & Related papers  (2020-05-26T09:18:14Z)

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.