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: CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length
CDSAT (Conflict-Driven Satisfiability) is a paradigm for theory combination that works by coordinating theory modules to reason in the union of the theories in a conflict-driven manner. We generalize CDSAT to the case of nondisjoint theories by presenting a new CDSAT theory module for a theory of arrays with abstract length, which is an abstraction of the theory of arrays with length. The length function is a bridging function as it forces theories to share symbols, but the proposed abstraction limits the sharing to one predicate symbol. The CDSAT framework handles shared predicates with minimal changes, and the new module satisfies the CDSAT requirements, so that completeness is preserved.  more » « less
Award ID(s):
1816936
PAR ID:
10358980
Author(s) / Creator(s):
; ;
Editor(s):
Deharbe, David; Hyvarinen, Antti E.
Date Published:
Journal Name:
Satisfiability Modulo Theories workshop, CEUR Workshop Proceedings
Volume:
3185
Page Range / eLocation ID:
18--37
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. ; ; (, Springer Nature Switzerland)
    Gurfinkel, Arie; Ganesh, Vijay (Ed.)
    Abstract The dominant state-of-the-art approach for solving bit-vector formulas in Satisfiability Modulo Theories (SMT) is bit-blasting, an eager reduction to propositional logic. Bit-blasting is surprisingly efficient in practice but does not generally scale well with increasing bit-widths, especially when bit-vector arithmetic is present. In this paper, we present a novel CEGAR-style abstraction-refinement procedure for the theory of fixed-size bit-vectors that significantly improves the scalability of bit-blasting. We provide lemma schemes for various arithmetic bit-vector operators and an abduction-based framework for synthesizing refinement lemmas. We extended the state-of-the-art SMT solver Bitwuzla with our abstraction-refinement approach and show that it significantly improves solver performance on a variety of benchmark sets, including industrial benchmarks that arise from smart contract verification. 
    more » « less
  4. (, Journal of elasticity)
    A dense closed cell foam is studied to determine which continuum theory of elasticity is applicable. Size effects inconsistent with classical elasticity are observed. The material exhibits a characteristic length scale considerably larger, by more than a factor 6, than the largest observable structure size. The Cosserat coupling number N is shown to be small, via measurements of size effects in square section bars, comparison with size effects in round section bars, and determination of warp of a square section bar in torsion. For this material, the couple stress theory is excluded and the modified couple stress theory is excluded. Theories that force constants to their thermodynamic limits do not apply to this foam. The role of other generalized continuum theories is considered. 
    more » « less
  5. ; ; (, eLife)
    To effectively interact with their environment, humans must often select actions from multiple incompatible options. Existing theories propose that during motoric response-conflict, inappropriate motor activity is actively (and perhaps non-selectively) suppressed by an inhibitory fronto-basal ganglia mechanism. We here tested this theory across three experiments. First, using scalp-EEG, we found that both outright action-stopping and response-conflict during action-selection invoke low-frequency activity of a common fronto-central source, whose activity relates to trial-by-trial behavioral indices of inhibition in both tasks. Second, using simultaneous intracranial recordings from the basal ganglia and motor cortex, we found that response-conflict increases the influence of the subthalamic nucleus on M1-representations of incorrect response-tendencies. Finally, using transcranial magnetic stimulation, we found that during the same time period when conflict-related STN-to-M1 communication is increased, cortico-spinal excitability is broadly suppressed. Together, these findings demonstrate that fronto-basal ganglia networks buttress action-selection under response-conflict by rapidly and non-selectively net-inhibiting inappropriate motor tendencies. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email