More Like this

1. Interpolation and Amalgamation for Arrays with MaxDiff

   https://doi.org/10.1007/978-3-030-71995-1_14  

   Ghilardi, Silvio; Gianola, Alessandro; Kapur, Deepak (January 2021, Springer International Publishing)

   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
2. AXDInterpolator: A Tool for Computing Interpolants for Arrays with MaxDiff

   Castellanos-Joo, Jose Abel; Ghilardi, Silvio; Gianola, Alessandro; Kapur, Deepak (July 2021, 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. CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length

   Bonacina, Maria Paola; Graham-Lengrand, Stephane; Shankar, Natarajan (August 2022, Satisfiability Modulo Theories workshop, CEUR Workshop Proceedings)

   Deharbe, David; Hyvarinen, Antti E. (Ed.)

   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
4. Zero-crosstalk silicon photonic refractive index sensor with subwavelength gratings

   https://doi.org/10.1186/s40580-024-00446-1  

   Ahmed, Syed_Z; Hasan, Mehedi; Kim, Kyungtae; Kim, Sangsik (September 2024, Nano Convergence)

   Abstract Silicon photonic index sensors have received significant attention for label-free bio and gas-sensing applications, offering cost-effective and scalable solutions. Here, we introduce an ultra-compact silicon photonic refractive index sensor that leverages zero-crosstalk singularity responses enabled by subwavelength gratings. The subwavelength gratings are precisely engineered to achieve an anisotropic perturbation-led zero-crosstalk, resulting in a single transmission dip singularity in the spectrum that is independent of device length. The sensor is optimized for the transverse magnetic mode operation, where the subwavelength gratings are arranged perpendicular to the propagation direction to support a leaky-like mode and maximize the evanescent field interaction with the analyte space. Experimental results demonstrate a high wavelength sensitivity of − 410 nm/RIU and an intensity sensitivity of 395 dB/RIU, with a compact device footprint of approximately 82.8 μm². Distinct from other resonant and interferometric sensors, our approach provides an FSR-free single-dip spectral response on a small device footprint, overcoming common challenges faced by traditional sensors, such as signal/phase ambiguity, sensitivity fading, limited detection range, and the necessity for large device footprints. This makes our sensor ideal for simplified intensity interrogation. The proposed sensor holds promise for a range of on-chip refractive index sensing applications, from gas to biochemical detection, representing a significant step towards efficient and miniaturized photonic sensing solutions. Graphical Abstract 

   more » « less
5. Mutual Information as a Function of Matrix SNR for Linear Gaussian Channels

   Reeves, Galen; Pfister, Henry D.; Dytso, Alex (July 2018, IEEE International Symposium on Information Theory)

   This paper focuses on the mutual information and minimum mean-squared error (MMSE) as a function a matrix- valued signal-to-noise ratio (SNR) for a linear Gaussian channel with arbitrary input distribution. As shown by Lamarca, the mutual-information is a concave function of a positive semi- definite matrix, which we call the matrix SNR. This implies that the mapping from the matrix SNR to the MMSE matrix is decreasing monotone. Building upon these functional properties, we start to construct a unifying framework that provides a bridge between classical information-theoretic inequalities, such as the entropy power inequality, and interpolation techniques used in statistical physics and random matrix theory. This framework provides new insight into the structure of phase transitions in coding theory and compressed sensing. In particular, it is shown that the parallel combination of linear channels with freely-independent matrices can be characterized succinctly via free convolution. 

   more » « less