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

      Interpolation and the Array Property Fragment

      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

          Interpolation based software model checkers have been successfully employed to automatically prove programs correct. Their power comes from interpolating SMT solvers that check the feasibility of potential counterexamples and compute candidate invariants, otherwise. This approach works well for quantifier-free theories, like equality theory or linear arithmetic. For quantified formulas, there are SMT solvers that can decide expressive fragments of quantified formulas, e. g., EPR, the array property fragment, and the finite almost uninterpreted fragment. However, these solvers do not support interpolation. It is already known that in general EPR does not allow for interpolation. In this paper, we show the same result for the array property fragment.

          Related collections

          Most cited references11

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

          Lazy Abstraction with Interpolants

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            An interpolating theorem prover

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

              Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories

                Bookmark

                Author and article information

                Journal
                25 April 2019
                Article
                1904.11381
                11031a39-0be0-487d-8dba-d9fbe08dd7c7

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

                History
                Custom metadata
                cs.LO

                Theoretical computer science
                Theoretical computer science

                Comments

                Comment on this article