skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


Title: Interpolation and Amalgamation for Arrays with MaxDiff
Abstract In this paper, the theory of McCarthy’s extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the extensionality axiom). Our maxdiff operation significantly increases the level of expressivity; however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and it is shown how to convert them into concrete interpolation algorithms via a hierarchical approach.  more » « less
Award ID(s):
1908804
PAR ID:
10642529
Author(s) / Creator(s):
; ;
Publisher / Repository:
Springer International Publishing
Date Published:
Page Range / eLocation ID:
268 to 288
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ; (, ACM Transactions on Computational Logic)
    In this article, we enrich McCarthy’s theory of extensional arrays with a length and a maxdiff operation. As is well-known, some diff operation (i.e., some kind of difference function showing where two unequal arrays differ) is needed to keep interpolants quantifier free in array theories. Our maxdiff operation returns the max index where two arrays differ; thus, it has a univocally determined semantics. The length function is a natural complement of such a maxdiff operation and is needed to handle real arrays. Obtaining interpolation results for such a rich theory is a surprisingly hard task. We get such results via a thorough semantic analysis of the models of the theory and of their amalgamation and strong amalgamation properties. The results are modular with respect to the index theory; we show how to convert them into concrete interpolation algorithms via a hierarchical approach realizing a polynomial reduction to interpolation in linear arithmetics endowed with free function symbols. 
    more » « less
  2. ; ; ; (, Unknown)
    Several approaches toward quantifier-free interpolation algorithms of theories involving arrays have been proposed by extending the language using a binary function skolemizing the extensionality principle. In FoSSaCS 2021, the last three authors studied the enrichment of the McCarthy’s theory of extensional arrays with a maxdiff operation. This paper discusses the implementation of the interpolation algorithm proposed in FoSSaCS 2021 using the Z3 API. The implementation allows the user to choose iZ3, Mathsat, or SMTInterpol as interpolation engines. The tool returns a formula in SMTLIB2 format, which allows compatibility with model checkers and invariant generators using such a format. We compare our algorithm with state-of-the-art interpolation engines. Our experiments using unsatisfiable formulæ extracted with the model checker UAutomizer show the feasibility of our tool. For that purpose, we used C programs from the ReachSafety-Arrays and MemSafety-Arrays tracks of SV-COMP. 
    more » « less
  3. ; ; ; ; ; ; ; ; ; (, Journal of Automated Reasoning)
    Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (Ed.)
    Dynamic arrays, also referred to as vectors, are fundamental data structures used in many programs. Modeling their semantics efficiently is crucial when reasoning about such programs. The theory of arrays is widely supported but is not ideal, because the number of elements is fixed (determined by its index sort) and cannot be adjusted, which is a problem, given that the length of vectors often plays an important role when reasoning about vector programs. In this paper, we propose reasoning about vectors using a theory of sequences. We introduce the theory, propose a basic calculus adapted from one for the theory of strings, and extend it to efficiently handle common vector operations. We prove that our calculus is sound and show how to construct a model when it terminates with a saturated configuration. Finally, we describe an implementation of the calculus in cvc5 and demonstrate its efficacy by evaluating it on verification conditions for smart contracts and benchmarks derived from existing array benchmarks. 
    more » « less
  4. ; ; ; ; ; ; ; ; ; (, International Joint Conference on Automated Reasoning (IJCAR))
    Blanchette, Jasmin; Kovacs, Laura; Pattinson, Dirk (Ed.)
    Dynamic arrays, also referred to as vectors, are fundamental data structures used in many programs. Modeling their semantics efficiently is crucial when reasoning about such programs. The theory of arrays is widely supported but is not ideal, because the number of elements is fixed (determined by its index sort) and cannot be adjusted, which is a problem, given that the length of vectors often plays an important role when reasoning about vector programs. In this paper, we propose reasoning about vectors using a theory of sequences. We introduce the theory, propose a basic calculus adapted from one for the theory of strings, and extend it to efficiently handle common vector operations. We prove that our calculus is sound and show how to construct a model when it terminates with a saturated configuration. Finally, we describe an implementation of the calculus in cvc5 and demonstrate its efficacy by evaluating it on verification conditions for smart contracts and benchmarks derived from existing array benchmarks. 
    more » « less
  5. ; ; ; ; ; ; ; ; (, American Journal of Physical Medicine & Rehabilitation)
    ObjectiveThis quasi-experimental study examined the effect of repetitive finger stimulation on brain activation in eight stroke and seven control subjects, measured by quantitative electroencephalogram. MethodsWe applied 5 mins of 2-Hz repetitive bilateral index finger transcutaneous electrical nerve stimulation and compared differences pre– and post–transcutaneous electrical nerve stimulation using quantitative electroencephalogram metrics delta/alpha ratio and delta-theta/alpha-beta ratio. ResultsBetween-group differences before and after stimulation were significantly different in the delta/alpha ratio (z= −2.88,P= 0.0040) and the delta-theta/alpha-beta ratio variables (z= −3.90 withP< 0.0001). Significant decrease in the delta/alpha ratio and delta-theta/alpha-beta ratio variables after the transcutaneous electrical nerve stimulation was detected only in the stroke group (delta/alpha ratio diff = 3.87,P= 0.0211) (delta-theta/alpha-beta ratio diff = 1.19,P= 0.0074). ConclusionsThe decrease in quantitative electroencephalogram metrics in the stroke group may indicate improved brain activity after transcutaneous electrical nerve stimulation. This finding may pave the way for a future novel therapy based on transcutaneous electrical nerve stimulation and quantitative electroencephalogram measures to improve brain recovery after stroke. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email