An official website of the United States government
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
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
- 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
-
-
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
-
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
-
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
-
Abstract This review is focused on tests of Einstein’s theory of general relativity with gravitational waves that are detectable by ground-based interferometers and pulsar-timing experiments. Einstein’s theory has been greatly constrained in the quasi-linear, quasi-stationary regime, where gravity is weak and velocities are small. Gravitational waves are allowing us to probe a complimentary, yet previously unexplored regime: the non-linear and dynamicalextreme gravity regime. Such a regime is, for example, applicable to compact binaries coalescing, where characteristic velocities can reach fifty percent the speed of light and gravitational fields are large and dynamical. This review begins with the theoretical basis and the predicted gravitational-wave observables of modified gravity theories. The review continues with a brief description of the detectors, including both gravitational-wave interferometers and pulsar-timing arrays, leading to a discussion of the data analysis formalism that is applicable for such tests. The review then discusses gravitational-wave tests using compact binary systems, and ends with a description of the first gravitational wave observations by advanced LIGO, the stochastic gravitational wave background observations by pulsar timing arrays, and the tests that can be performed with them.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- The DOI is not currently available.
