Showing 1–17 of 17 results for author: Bryant, R

Towards a Personal Health Large Language Model

Authors: Justin Cosentino, Anastasiya Belyaeva, Xin Liu, Nicholas A. Furlotte, Zhun Yang, Chace Lee, Erik Schenck, Yojan Patel, Jian Cui, Logan Douglas Schneider, Robby Bryant, Ryan G. Gomes, Allen Jiang, Roy Lee, Yun Liu, Javier Perez, Jameson K. Rogers, Cathy Speed, Shyam Tailor, Megan Walker, Jeffrey Yu, Tim Althoff, Conor Heneghan, John Hernandez, Mark Malhotra , et al. (9 additional authors not shown)

Abstract: In health, most large language model (LLM) research has focused on clinical tasks. However, mobile and wearable devices, which are rarely integrated into such tasks, provide rich, longitudinal data for personal health monitoring. Here we present Personal Health Large Language Model (PH-LLM), fine-tuned from Gemini for understanding and reasoning over numerical time-series personal health data. We… ▽ More In health, most large language model (LLM) research has focused on clinical tasks. However, mobile and wearable devices, which are rarely integrated into such tasks, provide rich, longitudinal data for personal health monitoring. Here we present Personal Health Large Language Model (PH-LLM), fine-tuned from Gemini for understanding and reasoning over numerical time-series personal health data. We created and curated three datasets that test 1) production of personalized insights and recommendations from sleep patterns, physical activity, and physiological responses, 2) expert domain knowledge, and 3) prediction of self-reported sleep outcomes. For the first task we designed 857 case studies in collaboration with domain experts to assess real-world scenarios in sleep and fitness. Through comprehensive evaluation of domain-specific rubrics, we observed that Gemini Ultra 1.0 and PH-LLM are not statistically different from expert performance in fitness and, while experts remain superior for sleep, fine-tuning PH-LLM provided significant improvements in using relevant domain knowledge and personalizing information for sleep insights. We evaluated PH-LLM domain knowledge using multiple choice sleep medicine and fitness examinations. PH-LLM achieved 79% on sleep and 88% on fitness, exceeding average scores from a sample of human experts. Finally, we trained PH-LLM to predict self-reported sleep quality outcomes from textual and multimodal encoding representations of wearable data, and demonstrate that multimodal encoding is required to match performance of specialized discriminative models. Although further development and evaluation are necessary in the safety-critical personal health domain, these results demonstrate both the broad knowledge and capabilities of Gemini models and the benefit of contextualizing physiological data for personal health applications as done with PH-LLM. △ Less

Submitted 10 June, 2024; originally announced June 2024.

Comments: 72 pages

Notes on "Bounds on BDD-Based Bucket Elimination''

Authors: Randal E. Bryant

Abstract: This paper concerns Boolean satisfiability (SAT) solvers based on Ordered Binary Decision Diagrams (BDDs), especially those that can generate proofs of unsatisfiability. Mengel (arXiv:2306.00886) has presented a theoretical analysis that a BDD-based SAT solver can generate a proof of unsatisfiability for the pigeonhole problem (PHP$_n$) in polynomial time, even when the problem is encoded in the s… ▽ More This paper concerns Boolean satisfiability (SAT) solvers based on Ordered Binary Decision Diagrams (BDDs), especially those that can generate proofs of unsatisfiability. Mengel (arXiv:2306.00886) has presented a theoretical analysis that a BDD-based SAT solver can generate a proof of unsatisfiability for the pigeonhole problem (PHP$_n$) in polynomial time, even when the problem is encoded in the standard ``direct'' form. His approach is based on bucket elimination, using different orderings for the variables in the BDDs than in the buckets. We show experimentally that these proofs scale as $O(n^5)$. We also confirm the exponential scaling that occurs when the same variable ordering is used for the BDDs as for the buckets. △ Less

Submitted 17 June, 2023; originally announced June 2023.

Comments: Unpublished note

ACM Class: F.4.1

Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination

Authors: Mate Soos, Randal E. Bryant

Abstract: Traditional Boolean satisfiability (SAT) solvers based on the conflict-driven clause-learning (CDCL) framework fare poorly on formulas involving large numbers of parity constraints. The CryptoMiniSat solver augments CDCL with Gauss-Jordan elimination to greatly improve performance on these formulas. Integrating the TBUDDY proof-generating BDD library into CryptoMiniSat enables it to generate unsat… ▽ More Traditional Boolean satisfiability (SAT) solvers based on the conflict-driven clause-learning (CDCL) framework fare poorly on formulas involving large numbers of parity constraints. The CryptoMiniSat solver augments CDCL with Gauss-Jordan elimination to greatly improve performance on these formulas. Integrating the TBUDDY proof-generating BDD library into CryptoMiniSat enables it to generate unsatisfiability proofs when using Gauss-Jordan elimination. These proofs are compatible with standard, clausal proof frameworks. △ Less

Submitted 9 April, 2023; originally announced April 2023.

Comments: Presented at 2022 Workshop on the Pragmatics of SAT

ACM Class: F.4.1

An Empirical Study of Accuracy, Fairness, Explainability, Distributional Robustness, and Adversarial Robustness

Authors: Moninder Singh, Gevorg Ghalachyan, Kush R. Varshney, Reginald E. Bryant

Abstract: To ensure trust in AI models, it is becoming increasingly apparent that evaluation of models must be extended beyond traditional performance metrics, like accuracy, to other dimensions, such as fairness, explainability, adversarial robustness, and distribution shift. We describe an empirical study to evaluate multiple model types on various metrics along these dimensions on several datasets. Our r… ▽ More To ensure trust in AI models, it is becoming increasingly apparent that evaluation of models must be extended beyond traditional performance metrics, like accuracy, to other dimensions, such as fairness, explainability, adversarial robustness, and distribution shift. We describe an empirical study to evaluate multiple model types on various metrics along these dimensions on several datasets. Our results show that no particular model type performs well on all dimensions, and demonstrate the kinds of trade-offs involved in selecting models evaluated along multiple dimensions. △ Less

Submitted 29 September, 2021; originally announced September 2021.

Journal ref: presented at the 2021 KDD Workshop on Measures and Best Practices for Responsible AI

Generating Extended Resolution Proofs with a BDD-Based SAT Solver

Authors: Randal E. Bryant, Marijn J. H. Heule

Abstract: In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in the extended resolution logical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability for a set of clauses. Such a proof in… ▽ More In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in the extended resolution logical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability for a set of clauses. Such a proof indicates that the formula is truly unsatisfiable without requiring the user to trust the BDD package or the SAT solver built on top of it. We extend their work to enable arbitrary existential quantification of the formula variables, a critical capability for BDD-based SAT solvers. We demonstrate the utility of this approach by applying a BDD-based solver, implemented by modifying an existing BDD package, to several challenging Boolean satisfiability problems. Our resultsdemonstrate scaling for parity formulas, as well as the Urquhart, mutilated chessboard, and pigeonhole problems far beyond that of other proof-generating SAT solvers. △ Less

Submitted 27 March, 2023; v1 submitted 3 May, 2021; originally announced May 2021.

Comments: Extended version of paper published at TACAS 2021

From Data to Knowledge to Action: Enabling the Smart Grid

Authors: Randal E. Bryant, Randy H. Katz, Chase Hensel, Erwin P. Gianchandani

Abstract: Our nation's infrastructure for generating, transmitting, and distributing electricity - "The Grid" - is a relic based in many respects on century-old technology. It consists of expensive, centralized generation via large plants, and a massive transmission and distribution system. It strives to deliver high-quality power to all subscribers simultaneously - no matter what their demand - and must th… ▽ More Our nation's infrastructure for generating, transmitting, and distributing electricity - "The Grid" - is a relic based in many respects on century-old technology. It consists of expensive, centralized generation via large plants, and a massive transmission and distribution system. It strives to deliver high-quality power to all subscribers simultaneously - no matter what their demand - and must therefore be sized to the peak aggregate demand at each distribution point. Ultimately, the system demands end-to-end synchronization, and it lacks a mechanism for storing ("buffering") energy, thus complicating sharing among grids or independent operation during an "upstream" outage. Recent blackouts demonstrate the existing grid's problems - failures are rare but spectacular. Moreover, the structure cannot accommodate the highly variable nature of renewable energy sources such as solar and wind. Many people are pinning their hopes on the "smart grid" - i.e., a more distributed, adaptive, and market-based infrastructure for the generation, distribution, and consumption of electrical energy. This new approach is designed to yield greater efficiency and resilience, while reducing environmental impact, compared to the existing electricity distribution system. Initial plans for the smart grid suggest it will make extensive use of existing information technology. In particular, recent advances in data analytics - i.e., data mining, machine learning, etc. - have the potential to greatly enhance the smart grid and, ultimately, amplify its impact, by helping us make sense of an increasing wealth of data about how we use energy and the kinds of demands that we are placing upon the current energy grid. Here we describe what the electricity grid could look like in 10 years, and specifically how Federal investment in data analytics approaches are critical to realizing this vision. △ Less

Submitted 31 July, 2020; originally announced August 2020.

Comments: A Computing Community Consortium (CCC) white paper, 8 pages

Nanotechnology-inspired Information Processing Systems of the Future

Authors: Randy Bryant, Mark Hill, Tom Kazior, Daniel Lee, Jie Liu, Klara Nahrstedt, Vijay Narayanan, Jan Rabaey, Hava Siegelmann, Naresh Shanbhag, Naveen Verma, H. -S. Philip Wong

Abstract: Nanoscale semiconductor technology has been a key enabler of the computing revolution. It has done so via advances in new materials and manufacturing processes that resulted in the size of the basic building block of computing systems - the logic switch and memory devices - being reduced into the nanoscale regime. Nanotechnology has provided increased computing functionality per unit volume, energ… ▽ More Nanoscale semiconductor technology has been a key enabler of the computing revolution. It has done so via advances in new materials and manufacturing processes that resulted in the size of the basic building block of computing systems - the logic switch and memory devices - being reduced into the nanoscale regime. Nanotechnology has provided increased computing functionality per unit volume, energy, and cost. In order for computing systems to continue to deliver substantial benefits for the foreseeable future to society at large, it is critical that the very notion of computing be examined in the light of nanoscale realities. In particular, one needs to ask what it means to compute when the very building block - the logic switch - no longer exhibits the level of determinism required by the von Neumann architecture. There needs to be a sustained and heavy investment in a nation-wide Vertically Integrated Semiconductor Ecosystem (VISE). VISE is a program in which research and development is conducted seamlessly across the entire compute stack - from applications, systems and algorithms, architectures, circuits and nanodevices, and materials. A nation-wide VISE provides clear strategic advantages in ensuring the US's global superiority in semiconductors. First, a VISE provides the highest quality seed-corn for nurturing transformative ideas that are critically needed today in order for nanotechnology-inspired computing to flourish. It does so by dramatically opening up new areas of semiconductor research that are inspired and driven by new application needs. Second, a VISE creates a very high barrier to entry from foreign competitors because it is extremely hard to establish, and even harder to duplicate. △ Less

Submitted 5 May, 2020; originally announced May 2020.

Comments: A Computing Community Consortium (CCC) workshop report, 18 pages

Report number: ccc2016report_3

ADW: Blockchain-enabled Small-scale Farm Digitization

Authors: Nelson Bore, Andrew Kinai, Peninah Waweru, Isaac Wambugu, Juliet Mutahi, Everlyne Kemunto, Reginald Bryant, Komminist Weldemariam

Abstract: Farm records hold the static, temporal, and longitudinal details of the farms. For small-scale farming, the ability to accurately capture these records plays a critical role in formalizing and digitizing the agriculture industry. Reliable exchange of these record through a trusted platform could unlock critical and valuable insights to different stakeholders across the value chain in agriculture e… ▽ More Farm records hold the static, temporal, and longitudinal details of the farms. For small-scale farming, the ability to accurately capture these records plays a critical role in formalizing and digitizing the agriculture industry. Reliable exchange of these record through a trusted platform could unlock critical and valuable insights to different stakeholders across the value chain in agriculture eco-system. Lately, there has been increasing attention on digitization of small scale farming with the objective of providing farm-level transparency, accountability, visibility, access to farm loans, etc. using these farm records. However, most solutions proposed so far have the shortcoming of providing detailed, reliable and trusted small-scale farm digitization information in real time. To address these challenges, we present a system, called Agribusiness Digital Wallet (ADW), which leverages blockchain to formalize the interactions and enable seamless data flow in small-scale farming ecosystem. Utilizing instrumentation of farm tractors, we demonstrate the ability to utilize farm activities to create trusted electronic field records (EFR) with automated valuable insights. Using ADW, we processed several thousands of small-scale farm-level activity events for which we also performed automated farm boundary detection of a number of farms in different geographies. △ Less

Submitted 15 March, 2020; originally announced March 2020.

Preservation of Anomalous Subgroups On Machine Learning Transformed Data

Authors: Samuel C. Maina, Reginald E. Bryant, William O. Goal, Robert-Florian Samoilescu, Kush R. Varshney, Komminist Weldemariam

Abstract: In this paper, we investigate the effect of machine learning based anonymization on anomalous subgroup preservation. In particular, we train a binary classifier to discover the most anomalous subgroup in a dataset by maximizing the bias between the group's predicted odds ratio from the model and observed odds ratio from the data. We then perform anonymization using a variational autoencoder (VAE)… ▽ More In this paper, we investigate the effect of machine learning based anonymization on anomalous subgroup preservation. In particular, we train a binary classifier to discover the most anomalous subgroup in a dataset by maximizing the bias between the group's predicted odds ratio from the model and observed odds ratio from the data. We then perform anonymization using a variational autoencoder (VAE) to synthesize an entirely new dataset that would ideally be drawn from the distribution of the original data. We repeat the anomalous subgroup discovery task on the new data and compare it to what was identified pre-anonymization. We evaluated our approach using publicly available datasets from the financial industry. Our evaluation confirmed that the approach was able to produce synthetic datasets that preserved a high level of subgroup differentiation as identified initially in the original dataset. Such a distinction was maintained while having distinctly different records between the synthetic and original dataset. Finally, we packed the above end to end process into what we call Utility Guaranteed Deep Privacy (UGDP) system. UGDP can be easily extended to onboard alternative generative approaches such as GANs to synthesize tabular data. △ Less

Submitted 9 November, 2019; originally announced November 2019.

Comments: 5 pages, 3 figures, 2 tables, submitted to icassp 2019

Analyzing Bias in Sensitive Personal Information Used to Train Financial Models

Authors: Reginald Bryant, Celia Cintas, Isaac Wambugu, Andrew Kinai, Komminist Weldemariam

Abstract: Bias in data can have unintended consequences that propagate to the design, development, and deployment of machine learning models. In the financial services sector, this can result in discrimination from certain financial instruments and services. At the same time, data privacy is of paramount importance, and recent data breaches have seen reputational damage for large institutions. Presented in… ▽ More Bias in data can have unintended consequences that propagate to the design, development, and deployment of machine learning models. In the financial services sector, this can result in discrimination from certain financial instruments and services. At the same time, data privacy is of paramount importance, and recent data breaches have seen reputational damage for large institutions. Presented in this paper is a trusted model-lifecycle management platform that attempts to ensure consumer data protection, anonymization, and fairness. Specifically, we examine how datasets can be reproduced using deep learning techniques to effectively retain important statistical features in datasets whilst simultaneously protecting data privacy and enabling safe and secure sharing of sensitive personal information beyond the current state-of-practice. △ Less

Submitted 9 November, 2019; originally announced November 2019.

Comments: 5 pages, 4 figures, IEEE Global Conference on Signal and Information Processing (GlobalSIP 2019)

Chain Reduction for Binary and Zero-Suppressed Decision Diagrams

Authors: Randal E. Bryant

Abstract: Chain reduction enables reduced ordered binary decision diagrams (BDDs) and zero-suppressed binary decision diagrams (ZDDs) to each take advantage of the others' ability to symbolically represent Boolean functions in compact form. For any Boolean function, its chain-reduced ZDD (CZDD) representation will be no larger than its ZDD representation, and at most twice the size of its BDD representation… ▽ More Chain reduction enables reduced ordered binary decision diagrams (BDDs) and zero-suppressed binary decision diagrams (ZDDs) to each take advantage of the others' ability to symbolically represent Boolean functions in compact form. For any Boolean function, its chain-reduced ZDD (CZDD) representation will be no larger than its ZDD representation, and at most twice the size of its BDD representation. The chain-reduced BDD (CBDD) of a function will be no larger than its BDD representation, and at most three times the size of its CZDD representation. Extensions to the standard algorithms for operating on BDDs and ZDDs enable them to operate on the chain-reduced versions. Experimental evaluations on representative benchmarks for encoding word lists, solving combinatorial problems, and operating on digital circuits indicate that chain reduction can provide significant benefits in terms of both memory and execution time. △ Less

Submitted 17 October, 2017; originally announced October 2017.

Advances in Artificial Intelligence Require Progress Across all of Computer Science

Authors: Gregory D. Hager, Randal Bryant, Eric Horvitz, Maja Mataric, Vasant Honavar

Abstract: Advances in Artificial Intelligence require progress across all of computer science. Advances in Artificial Intelligence require progress across all of computer science. △ Less

Submitted 13 July, 2017; originally announced July 2017.

Comments: 7 pages, Computing Community Consortium White Paper

CommuniSense: Crowdsourcing Road Hazards in Nairobi

Authors: Darshan Santani, Jidraph Njuguna, Tierra Bills, Aisha W. Bryant, Reginald Bryant, Jonathan Ledgard, Daniel Gatica-Perez

Abstract: Nairobi is one of the fastest growing metropolitan cities and a major business and technology powerhouse in Africa. However, Nairobi currently lacks monitoring technologies to obtain reliable data on traffic and road infrastructure conditions. In this paper, we investigate the use of mobile crowdsourcing as means to gather and document Nairobi's road quality information. We first present the key f… ▽ More Nairobi is one of the fastest growing metropolitan cities and a major business and technology powerhouse in Africa. However, Nairobi currently lacks monitoring technologies to obtain reliable data on traffic and road infrastructure conditions. In this paper, we investigate the use of mobile crowdsourcing as means to gather and document Nairobi's road quality information. We first present the key findings of a city-wide road quality survey about the perception of existing road quality conditions in Nairobi. Based on the survey's findings, we then developed a mobile crowdsourcing application, called CommuniSense, to collect road quality data. The application serves as a tool for users to locate, describe, and photograph road hazards. We tested our application through a two-week field study amongst 30 participants to document various forms of road hazards from different areas in Nairobi. To verify the authenticity of user-contributed reports from our field study, we proposed to use online crowdsourcing using Amazon's Mechanical Turk (MTurk) to verify whether submitted reports indeed depict road hazards. We found 92% of user-submitted reports to match the MTurkers judgements. While our prototype was designed and tested on a specific city, our methodology is applicable to other developing cities. △ Less

Submitted 24 June, 2015; originally announced June 2015.

Comments: In Proceedings of 17th International Conference on Human-Computer Interaction with Mobile Devices and Services (MobileHCI 2015)

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds

Authors: Sanjit A. Seshia, Randal E. Bryant

Abstract: Given a formula in quantifier-free Presburger arithmetic, if it has a satisfying solution, there is one whose size, measured in bits, is polynomially bounded in the size of the formula. In this paper, we consider a special class of quantifier-free Presburger formulas in which most linear constraints are difference (separation) constraints, and the non-difference constraints are sparse. This clas… ▽ More Given a formula in quantifier-free Presburger arithmetic, if it has a satisfying solution, there is one whose size, measured in bits, is polynomially bounded in the size of the formula. In this paper, we consider a special class of quantifier-free Presburger formulas in which most linear constraints are difference (separation) constraints, and the non-difference constraints are sparse. This class has been observed to commonly occur in software verification. We derive a new solution bound in terms of parameters characterizing the sparseness of linear constraints and the number of non-difference constraints, in addition to traditional measures of formula size. In particular, we show that the number of bits needed per integer variable is linear in the number of non-difference constraints and logarithmic in the number and size of non-zero coefficients in them, but is otherwise independent of the total number of linear constraints in the formula. The derived bound can be used in a decision procedure based on instantiating integer variables over a finite domain and translating the input quantifier-free Presburger formula to an equi-satisfiable Boolean formula, which is then checked using a Boolean satisfiability solver. In addition to our main theoretical result, we discuss several optimizations for deriving tighter bounds in practice. Empirical evidence indicates that our decision procedure can greatly outperform other decision procedures. △ Less

Submitted 7 October, 2008; v1 submitted 5 August, 2005; originally announced August 2005.

Comments: 26 pages

ACM Class: I.2.3; F.4.1; F.3.1

Journal ref: Logical Methods in Computer Science, Volume 1, Issue 2 (December 19, 2005) lmcs:2270

Predicate Abstraction with Indexed Predicates

Authors: Shuvendu K. Lahiri, Randal E. Bryant

Abstract: Predicate abstraction provides a powerful tool for verifying properties of infinite-state systems using a combination of a decision procedure for a subset of first-order logic and symbolic methods originally developed for finite-state model checking. We consider models containing first-order state variables, where the system state includes mutable functions and predicates. Such a model can descr… ▽ More Predicate abstraction provides a powerful tool for verifying properties of infinite-state systems using a combination of a decision procedure for a subset of first-order logic and symbolic methods originally developed for finite-state model checking. We consider models containing first-order state variables, where the system state includes mutable functions and predicates. Such a model can describe systems containing arbitrarily large memories, buffers, and arrays of identical processes. We describe a form of predicate abstraction that constructs a formula over a set of universally quantified variables to describe invariant properties of the first-order state variables. We provide a formal justification of the soundness of our approach and describe how it has been used to verify several hardware and software designs, including a directory-based cache coherence protocol. △ Less

Submitted 2 July, 2004; originally announced July 2004.

Comments: 27 pages, 4 figures, 1 table, short version appeared in International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04), LNCS 2937, pages = 267--281

ACM Class: F.3.1

Boolean Satisfiability with Transitivity Constraints

Authors: Randal E. Bryant, Miroslav N. Velev

Abstract: We consider a variant of the Boolean satisfiability problem where a subset E of the propositional variables appearing in formula Fsat encode a symmetric, transitive, binary relation over N elements. Each of these relational variables, e[i,j], for 1 <= i < j <= N, expresses whether or not the relation holds between elements i and j. The task is to either find a satisfying assignment to Fsat that… ▽ More We consider a variant of the Boolean satisfiability problem where a subset E of the propositional variables appearing in formula Fsat encode a symmetric, transitive, binary relation over N elements. Each of these relational variables, e[i,j], for 1 <= i < j <= N, expresses whether or not the relation holds between elements i and j. The task is to either find a satisfying assignment to Fsat that also satisfies all transitivity constraints over the relational variables (e.g., e[1,2] & e[2,3] ==> e[1,3]), or to prove that no such assignment exists. Solving this satisfiability problem is the final and most difficult step in our decision procedure for a logic of equality with uninterpreted functions. This procedure forms the core of our tool for verifying pipelined microprocessors. To use a conventional Boolean satisfiability checker, we augment the set of clauses expressing Fsat with clauses expressing the transitivity constraints. We consider methods to reduce the number of such clauses based on the sparse structure of the relational variables. To use Ordered Binary Decision Diagrams (OBDDs), we show that for some sets E, the OBDD representation of the transitivity constraints has exponential size for all possible variable orderings. By considering only those relational variables that occur in the OBDD representation of Fsat, our experiments show that we can readily construct an OBDD representation of the relevant transitivity constraints and thus solve the constrained satisfiability problem. △ Less

Submitted 1 August, 2000; originally announced August 2000.

Comments: Submitted to ACM Transactions on Computational Logic

ACM Class: I2.3; G2.2

Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic

Authors: Randal E. Bryant, Steven German, Miroslav N. Velev

Abstract: The logic of equality with uninterpreted functions (EUF) provides a means of abstracting the manipulation of data by a processor when verifying the correctness of its control logic. By reducing formulas in this logic to propositional formulas, we can apply Boolean methods such as Ordered Binary Decision Diagrams (BDDs) and Boolean satisfiability checkers to perform the verification. We can exp… ▽ More The logic of equality with uninterpreted functions (EUF) provides a means of abstracting the manipulation of data by a processor when verifying the correctness of its control logic. By reducing formulas in this logic to propositional formulas, we can apply Boolean methods such as Ordered Binary Decision Diagrams (BDDs) and Boolean satisfiability checkers to perform the verification. We can exploit characteristics of the formulas describing the verification conditions to greatly simplify the propositional formulas generated. In particular, we exploit the property that many equations appear only in positive form. We can therefore reduce the set of interpretations of the function symbols that must be considered to prove that a formula is universally valid to those that are ``maximally diverse.'' We present experimental results demonstrating the efficiency of this approach when verifying pipelined processors using the method proposed by Burch and Dill. △ Less

Submitted 6 July, 2000; v1 submitted 14 October, 1999; originally announced October 1999.

Comments: 46 pages

ACM Class: F.4.1