21
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Interpolating Strong Induction

      Preprint
      , , ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          The principle of strong induction, also known as k-induction is one of the first techniques for unbounded SAT-based Model Checking (SMC). While elegant and simple to apply, properties as such are rarely k-inductive and when they can be strengthened, there is no effective strategy to guess the depth of induction. It has been mostly displaced by techniques that compute inductive strengthenings based on interpolation and property directed reachability (Pdr). In this paper, we present kAvy, an SMC algorithm that effectively uses k-induction to guide interpolation and Pdr-style inductive generalization. Unlike pure k-induction, kAvy uses Pdr-style generalization to compute and strengthen an inductive trace. Unlike pure Pdr, kAvy uses relative k-induction to construct an inductive invariant. The depth of induction is adjusted dynamically by minimizing a proof of unsatisfiability. We have implemented kAvy within the Avy Model Checker and evaluated it on HWMCC instances. Our results show that kAvy is more effective than both Avy and Pdr, and that using k-induction leads to faster running time and solving more instances. Further, on a class of benchmarks, called shift, kAvy is orders of magnitude faster than Avy, Pdr and k-induction.

          Related collections

          Most cited references14

          • Record: found
          • Abstract: not found
          • Book Chapter: not found

          Symbolic Model Checking without BDDs

            Bookmark
            • Record: found
            • Abstract: not found
            • Book Chapter: not found

            Interpolation and SAT-Based Model Checking

              Bookmark
              • Record: found
              • Abstract: not found
              • Book Chapter: not found

              Horn Clause Solvers for Program Verification

                Bookmark

                Author and article information

                Journal
                04 June 2019
                Article
                1906.01583
                273244dc-8ba0-4beb-962c-145d14c44e10

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                Accepted to CAV 19
                cs.LO

                Theoretical computer science
                Theoretical computer science

                Comments

                Comment on this article