More Like this

1. Scalable Bit-Blasting with Abstractions

   https://doi.org/10.1007/978-3-031-65627-9_9  

   Niemetz, Aina; Preiner, Mathias; Zohar, Yoni (January 2024, 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
2. EMC: Efficient Muller C-Element Implementation for High Bit-width Asynchronous Applications

   Emmert, John Martin; VanDewerker, Sara A. (July 2021, 64th IEEE International Midwest Symposium on Circuits and Systems)

   null (Ed.)

   A Muller C-Element is a digital circuit component used in most asynchronous circuits and systems. In Null Convention Logic, the Muller C-Elements make up the subset of THmn threshold gates where the threshold, m, and the input bit- width, n, are equal. This paper presents a new Efficient Muller C- Element implementation, EMC, that is especially suitable for Null Convention Logic applications with high input bit-widths, and it is much faster and smaller than standard implementations. It has a two-transistor switching delay that is independent of the input bit- width, n, and exhibits low noise and static power consumption. It is suitable for all Muller C-Element applications, especially those like Null Convention Logic register feedback circuits that can have large input bit-widths. To reduce static power consumption, it uses active resistors that are only turned “ON” when necessary. Two output stages are presented to implement the required Muller C- Element digital hysteresis: standard, semi-static cross-coupled inverter version, and differential sense-amplifier option. For large values of n, our circuit requires approximately one-half fewer transistors than combining smaller Null Convention Logic THmn semi-static threshold gates. We have successfully simulated up to n = 1024 at a 65 nm node. 

   more » « less
3. Mycielski Graphs and PR Proofs

   https://doi.org/10.1007/978-3-030-51825-7_15  

   Yolcu, Emre; Wu, Xinyu; Heule, Marijn (June 2020, Theory and Applications of Satisfiability Testing – SAT 2020)

   Mycielski graphs are a family of triangle-free graphs 𝑀_𝑘 with arbitrarily high chromatic number. 𝑀_𝑘 has chromatic number k and there is a short informal proof of this fact, yet finding proofs of it via automated reasoning techniques has proved to be a challenging task. In this paper, we study the complexity of clausal proofs of the uncolorability of 𝑀_𝑘 with 𝑘−1 colors. In particular, we consider variants of the PR (propagation redundancy) proof system that are without new variables, and with or without deletion. These proof systems are of interest due to their potential uses for proof search. As our main result, we present a sublinear-length and constant-width PR proof without new variables or deletion. We also implement a proof generator and verify the correctness of our proof. Furthermore, we consider formulas extended with clauses from the proof until a short resolution proof exists, and investigate the performance of CDCL in finding the short proof. This turns out to be difficult for CDCL with the standard heuristics. Finally, we describe an approach inspired by SAT sweeping to find proofs of these extended formulas. 

   more » « less
4. Towards Certified Meta-Programming with Typed Template-Coq

   Abhishek Anand, Simon Boulier (July 2018, ITP 2018 - 9th Conference on Interactive Theorem Proving)

   Template-Coq 5 is a plugin for Coq, originally implemented by Malecha, which provides a reifier for Coq terms and global declara- tions, as represented in the Coq kernel, as well as a denotation command. Initially, it was developed for the purpose of writing functions on Coq’s AST in Gallina. Recently, it was used in the CertiCoq certified compiler project, as its front-end language, to derive parametricity properties, and to extract Coq terms to a CBV λ-calculus. However, the syntax lacked semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in Coq, the semantics of Coq’s type theory itself. The tool was also rather bare bones, providing only rudimentary quoting and unquoting commands. We generalize it to han- dle the entire Calculus of Inductive Constructions (CIC), as implemented by Coq, including the kernel’s declaration structures for definitions and inductives, and implement a monad for general manipulation of Coq’s logical environment. We demonstrate how this setup allows Coq users to define many kinds of general purpose plugins, whose correctness can be readily proved in the system itself, and that can be run efficiently after extraction. We give a few examples of implemented plugins, including a parametricity translation. We also advocate the use of Template-Coq as a foundation for higher-level tools. 

   more » « less
5. The width of Herschel filaments varies with distance

   https://doi.org/10.1051/0004-6361/202142281  

   Panopoulou, G. V.; Clark, S. E.; Hacar, A.; Heitsch, F.; Kainulainen, J.; Ntormousi, E.; Seifried, D.; Smith, R. J. (January 2022, Astronomy & Astrophysics)

   Context. Filamentary structures in nearby molecular clouds have been found to exhibit a characteristic width of 0.1 pc, as observed in dust emission. Understanding the origin of this universal width has become a topic of central importance in the study of molecular cloud structure and the early stages of star formation. Aims. We investigate how the recovered widths of filaments depend on the distance from the observer by using previously published results from the Herschel Gould Belt Survey. Methods. We obtained updated estimates on the distances to nearby molecular clouds observed with Herschel by using recent results based on 3D dust extinction mapping and Gaia . We examined the widths of filaments from individual clouds separately, as opposed to treating them as a single population. We used these per-cloud filament widths to search for signs of variation amongst the clouds of the previously published study. Results. We find a significant dependence of the mean per-cloud filament width with distance. The distribution of mean filament widths for nearby clouds is incompatible with that of farther away clouds. The mean per-cloud widths scale with distance approximately as 4−5 times the beam size. We examine the effects of resolution by performing a convergence study of a filament profile in the Herschel image of the Taurus Molecular Cloud. We find that resolution can severely affect the shapes of radial profiles over the observed range of distances. Conclusions. We conclude that the data are inconsistent with 0.1 pc being the universal characteristic width of filaments. 

   more » « less