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: AXDInterpolator: A Tool for Computing Interpolants for Arrays with MaxDiff
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
Award ID(s):
1908804
PAR ID:
10642532
Author(s) / Creator(s):
; ; ;
Date Published:
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; (, International Conference on ReConFigurable Computing and FPGAs (ReConFig))
    The processing demands of current and emerging applications, such as image/video processing, are increasing due to the deluge of data, generated by mobile and edge devices. This raises challenges for a vast range of computing systems, starting from smart-phones and reaching cloud and data centers. Heterogeneous computing demonstrates its ability as an efficient computing model due to its capability to adapt to various workload requirements. Field programmable gate arrays (FPGAs) provide power and performance benefits and have been used in many application domains from embedded systems to the cloud. In this paper, we used a closely coupled CPU-FPGA heterogeneous system to accelerate a sliding window based image processing algorithm, Canny edge detector. We accelerated Canny using two different implementations: Code partitioned and data partitioned. In the data partitioned implementation, we proposed a weighted round-robin based algorithm that partitions input images and distributes the load between the CPU and the FPGA based on latency. The paper also compares the performance of the proposed accelerators with separate CPU and FPGA implementations. Using our hybrid CPU-FPGA based algorithm, we achieved a speedup of up to 4.8× over a CPU-only and up to 2.1× over a FPGA-only implementations. Moreover, the estimated total energy consumption of our algorithm is more efficient than a CPU-only implementation. Our results show a significant reduction in energy-delay product (EDP) compared to the CPU-only implementation, and comparable EDP results to the FPGA-only implementation. 
    more » « less
  2. ; ; (, 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
  3. ; ; (, npj 2D Materials and Applications)
    Abstract Recent studies of resistive switching devices with hexagonal boron nitride (h-BN) as the switching layer have shown the potential of two-dimensional (2D) materials for memory and neuromorphic computing applications. The use of 2D materials allows scaling the resistive switching layer thickness to sub-nanometer dimensions enabling devices to operate with low switching voltages and high programming speeds, offering large improvements in efficiency and performance as well as ultra-dense integration. These characteristics are of interest for the implementation of neuromorphic computing and machine learning hardware based on memristor crossbars. However, existing demonstrations of h-BN memristors focus on single isolated device switching properties and lack attention to fundamental machine learning functions. This paper demonstrates the hardware implementation of dot product operations, a basic analog function ubiquitous in machine learning, using h-BN memristor arrays. Moreover, we demonstrate the hardware implementation of a linear regression algorithm on h-BN memristor arrays. 
    more » « less
  4. ; ; ; (, 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
  5. ; ; ; ; (, Proceedings of the ACM on Programming Languages)
    Modern web browsers rely on layout engines to convert HTML documents to layout trees that specify color, size, and position. However, existing layout engines are notoriously difficult to maintain because of the complexity of web standards. This is especially true for incremental layout engines, which are designed to improve performance by updating only the parts of the layout tree that need to be changed. In this paper, we propose Medea, a new framework for automatically generating incremental layout engines. Medea separates the specification of the layout engine from its incremental implementation, and guarantees correctness through layout engine synthesis. The synthesis is driven by a new iterative algorithm based on detecting conflicts that prevent optimality of the incremental algorithm. We evaluated Medea on a fragment of HTML layout that includes challenging features such as margin collapse, floating layout, and absolute positioning. Medea successfully synthesized an incremental layout engine for this fragment. The synthesized layout engine is both correct and efficient. In particular, we demonstrated that it avoids real-world bugs that have been reported in the layout engines of Chrome, Firefox, and Safari. The incremental layout engine synthesized by Medea is up to 1.82× faster than a naive incremental baseline. We also demonstrated that our conflict-driven algorithm produces engines that are 2.74× faster than a baseline without conflict analysis. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email