56 Result(s)
within
Chapter
Sharad Malik
-
Chapter and Conference Paper
Parallel Assertions for Architectures with Weak Memory Models
Assertions are a powerful and widely used debugging tool in sequential programs, but are ineffective at detecting concurrency bugs. We recently introduced parallel assertions which solve this problem by provid...
-
Chapter and Conference Paper
Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search
In our recent work, we addressed the problem of detecting serializability violations in a concurrent program using predictive analysis, where we used a graph-based method to derive a predictive model from a gi...
-
Chapter and Conference Paper
Parameterized Model Checking of Fine Grained Concurrency
Concurrent data structures are provided in libraries such as Intel Thread Building Blocks and Java.util.concurrent to enable efficient implementation of multi-threaded programs. Their efficiency is achieved by...
-
Chapter and Conference Paper
Hardware Verification: Techniques, Methodology and Solutions
Hardware verification has been one of the biggest drivers of formal verification research, and has seen the greatest practical impact of its results. The use of formal techniques has not been uniformly success...
-
Chapter and Conference Paper
Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares
Traditionally the propositional part of a Quantified Boolean Formula (QBF) instance has been represented using a conjunctive normal form (CNF). As with propositional satisfiability (SAT), this is motivated by ...
-
Chapter and Conference Paper
Lemma Learning in SMT on Linear Constraints
The past decade has seen great improvement in Boolean Satisfiability(SAT) solvers. SAT solving is now widely used in different areas, including electronic design automation, software verification and artificia...
-
Chapter and Conference Paper
On Solving the Partial MAX-SAT Problem
Boolean Satisfiability (SAT) has seen many successful applications in various fields such as Electronic Design Automation and Artificial Intelligence. However, in some cases, it may be required/preferable to u...
-
Chapter and Conference Paper
A Case for Runtime Validation of Hardware
Increasing hardware design complexity has resulted in significant challenges for hardware design verification. The growing “verification gap” between the complexity of what we can verify and what we can fabric...
-
Chapter and Conference Paper
Symmetry Reduction in SAT-Based Model Checking
The major challenge facing model checking is the state explosion problem. One technique to alleviate this is to apply symmetry reduction; this exploits the fact that many sequential systems consist of intercha...
-
Chapter and Conference Paper
Analysis of Search Based Algorithms for Satisfiability of Propositional and Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems
The sequential circuit state space diameter problem is an important problem in sequential verification. Bounded model checking is complete if the state space diameter of the system is known. By unrolling the t...
-
Chapter and Conference Paper
Zchaff2004: An Efficient SAT Solver
The Boolean Satisfiability Problem (SAT) is a well known NP-Complete problem. While its complexity remains a source of many interesting questions for theoretical computer scientists, the problem has found many...
-
Chapter and Conference Paper
Cache Performance of SAT Solvers: a Case Study for Efficient Implementation of Algorithms
We experimentally evaluate the cache performance of different SAT solvers as a case study for the efficient implementation of SAT algorithms. We evaluate several different Boolean Constraint Propagation (BCP) ...
-
Chapter
Modeling and Integration of Peripheral Devices in Embedded Systems
This paper describes automation methods for device driver development in IP-based embedded systems in order to achieve high reliability, productivity, reusability and fast time to market. We formally specify d...
-
Chapter
Power Analysis of Embedded Software: First Step Towards Software Power Minimization
Embedded computer systems are characterized by the presence of a dedicated processor and the software that runs on it. Power constraints are increasingly becoming the critical component of the design specifica...
-
Chapter and Conference Paper
The Quest for Efficient Boolean Satisfiability Solvers
The classical NP-complete problem of Boolean Satisfiability (SAT) has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem enab...
-
Chapter and Conference Paper
Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation
In this paper, we describe a new framework for evaluating Quantified Boolean Formulas (QBF). The new framework is based on the Davis-Putnam (DPLL) search algorithm. In existing DPLL based QBF algorithms, the p...
-
Chapter and Conference Paper
Design Tools for Application Specific Embedded Processors
A variety of factors make it increasingly difficult and expensive to design and manufacture traditional Application Specific Integrated Circuits (ASICs). Consequently, programmable alternatives are more attrac...
-
Chapter
Sat and ATPG: Algorithms for Boolean Decision Problems
The problems of Boolean satisfiability (SAT) and automatic test pattern generation (ATPG) are strongly related — both in terms of application areas (pre-manufacturing design validation and post-manufacturing test...
-
Chapter
Challenges in Code Generation for Embedded Processors
The emergence of integrated circuits in which both the program-ROM and the processor are integrated on a single die initiates a new era of problems for programming language compilers. In such a micro-architect...
-
Chapter and Conference Paper
The Quest for Efficient Boolean Satisfiability Solvers
The classical NP-complete problem of Boolean Satisfiability (SAT) has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem enab...
