Modular SMT-Based Verification of Rule-Based Hardware Designs by Wright, Andrew C.

“…This thesis aims to make hardware verification easier by leveraging the rule-level abstraction for verification using SMT-based verification, e.g. bounded and unbounded model checking. …”
Get full text

Smten and the art of satisfiability-based search by Uhler, Richard Stephen

Get full text

Synthesis of domain specific CNF encoders for bit-vector solvers by Inala, Jeevana Priya

Get full text

Polite Combination of Algebraic Datatypes by Sheng, Ying, Zohar, Yoni, Ringeissen, Christophe, Lange, Jane, Fontaine, Pascal, Barrett, Clark

“…Abstract Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. …”
Get full text

Using linguistic knowledge in statistical machine translation by Zbib, Rabih M. (Rabih Mohamed), 1974-

Get full text

Sterol and genomic analyses validate the sponge biomarker hypothesis by de Mendoza, Alex, Riesgo, Ana, Ruiz-Trillo, Iñaki, Summons, Roger E., Grabenstatter, Jonathan Dean, Gold, David

“…Using a molecular clock approach, we demonstrate that the relevant sponge SMT duplication event overlapped with the appearance of 24-isopropylcholestanes in the Neoproterozoic, but that the algal SMT duplication event occurred later in the Phanerozoic. …”
Get full text
Get full text
Get full text

Surface mounted PCB cleaning process improvement and Its impact on manufacturing system performance by Rajendran, Nikith

Get full text

Trigger Selection Strategies to Stabilize Program Verifiers by Leino, K. Rustan M., Pit-Claudel, Clement F.

“…SMT-based program verifiers often suffer from the so-called butterfly effect, in which minor modifications to the program source cause significant instabilities in verification times, which in turn may lead to spurious verification failures and a degraded user experience. …”
Get full text
Get full text

Trigger Selection Strategies to Stabilize Program Verifiers by Leino, K. Rustan M., Pit-Claudel, Clément

“…SMT-based program verifiers often suffer from the so-called butterfly effect, in which minor modifications to the program source cause significant instabilities in verification times, which in turn may lead to spurious verification failures and a degraded user experience. …”
Get full text
Get full text

Synthesizing a synthesis tool by Singh, Rohit, Ph. D. Massachusetts Institute of Technology.

Get full text

CONSTRAINING THE STRUCTURE OF SAGITTARIUS A*'s ACCRETION FLOW WITH MILLIMETER VERY LONG BASELINE INTERFEROMETRY CLOSURE PHASES by Broderick, Avery E., Fish, Vincent L., Doeleman, Sheperd Samuel, Loeb, Abraham

“…We find that the accretion flow models are capable of producing a wide variety of closure phases on the SMT-CARMA-JCMT triangle and thus not all models are consistent with the recent observations. …”
Get full text

Results and Analysis of SyGuS-Comp'15 by Alur, Rajeev, Fisman, Dana, Singh, Rishabh, Solar Lezama, Armando

“…In this year's competition we added two specialized tracks: a track for conditional linear arithmetic, where the grammar need not be specified and is implicitly assumed to be that of the LIA logic of SMT-LIB, and a track for invariant synthesis problems, with special constructs conforming to the structure of an invariant synthesis problem. …”
Get full text
Get full text

Proteomic responses of oceanic Synechococcus WH8102 to phosphate and zinc scarcity and cadmium additions by Cox, Alysia D., Saito, Mak A.

“…Similar trends in alkaline phosphate (ALP) and SmtA suggest the possibility of a Zn supply system to provide Zn to ALP that involves SmtA. …”
Get full text

Multiple sulfur isotopes discriminate organoclastic and methane-based sulfate reduction by sub-seafloor pyrite formation by Liu, Jiarui, Pellerin, André, Wang, Jiasheng, Rickard, David, Antler, Gilad, Zhao, Jie, Wang, Zhou, Jørgensen, Bo Barker, Ono, Shuhei

“…This is consistent with the slowly migrating sulfate–methane transition (SMT) in slope sediments inferred from sulfur and iron speciation, carbon isotope ratios of carbonates, and magnetic susceptibility data. …”
Get full text

Delta-Decision Procedures for Exists-Forall Problems over the Reals by Kong, Soonho, Solar-Lezama, Armando, Gao, Sicun

“…We propose δ -complete decision procedures for solving satisfiability of nonlinear SMT problems over real numbers that contain universal quantification and a wide range of nonlinear functions. …”
Get full text

SyGuS-Comp 2017: Results and Analysis by Alur, Rajeev, Fisman, Dana, Singh, Rishabh, Solar-Lezama, Armando

“…Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB. The Syntax-Guided Synthesis Competition (SyGuS-Comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. …”
Get full text

Alloy*: A Higher-Order Relational Constraint Solver by Milicevic, Aleksandar, Near, Joseph P., Kang, Eunsuk, Jackson, Daniel

“…Some tasks, however, most notably those involving synthesis, are inherently higher order; these are typically handled by embedding a first-order solver (such as a SAT or SMT solver) in a domain-specific algorithm. Using strategies similar to those used in such algorithms, we show how to extend a first-order solver (in this case Kodkod, a model finder for relational logic used as the engine of the Alloy Analyzer) so that it can handle quantifications over higher-order structures. …”
Get full text

Stepwise refinement of heap-manipulating code in Chalice by Leino, K. Rustan M., Yessenov, Kuat T

“…This paper describes a system with automated tool support for refinement, powered by a state-of-the-art verification engine that uses an SMT solver. Unlike previous refinement systems, users of the presented system interact only via declarations in the programming language. …”
Get full text
Get full text

A fully verified container library by Tschannen, Julian, Furia, Carlo A., Polikarpova, Nadezhda

“…Keywords: Deductive verification; SMT; Object-oriented software; Containers; AutoProof…”
Get full text
Get full text

SyGuS-Comp 2016: Results and Analysis by Alur, Rajeev, Fisman, Dana, Singh, Rishabh, Solar-Lezama, Armando

“…Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB. The Syntax-Guided Synthesis Competition (SyGuS-Comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. …”
Get full text