CHARME 2005 - PDF Preprint Papers

CHARME 2005 Correct Hardware Design and Verification Methods

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed CHARME-2005 Paper

click to vote

CHARME
2005
Springer

176views Hardware» more CHARME 2005»

An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment

14 years 5 months ago

Download www.cadence.com

Abstract. Model checking is a formal technique for automatically verifying that a ﬁnite-state model satisﬁes a temporal property. In model checking, generally Binary Decision D...

Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P...

claim paper

Read More »

Disclaimer and Copyright Notice

Sciweavers respects the rights of all copyright holders and in this regard, authors are only allowed to share a link to their preprint paper on their own website. Every contribution is associated with a desciptive image. It is the sole responsibility of the authors to ensure that their posted image is not copyright infringing. This service is compliant with IEEE copyright.

Id	Views	Title	Status

1	176	An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment	claim
2	170	Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification	claim
3	145	Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies	claim
4	143	Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning	claim
5	136	Acceleration of SAT-Based Iterative Property Checking	claim
6	136	Predictive Reachability Using a Sample-Based Approach	claim
7	133	Symbolic Partial Order Reduction for Rule Based Transition Systems	claim
8	130	Improvements to the Implementation of Interpolant-Based Model Checking	claim
9	128	Real-Time Model Checking Is Really Simple	claim
10	124	A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems	claim
11	124	Finding and Fixing Faults	claim
12	122	Regular Vacuity	claim
13	120	How Thorough Is Thorough Enough?	claim
14	120	Minimizing Counterexample of ACTL Property	claim
15	119	High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design	claim
16	106	Error Detection Using BMC in a Parallel Environment	claim
17	94	Verifying Quantitative Properties Using Bound Functions	claim
18	91	Temporal Modalities for Concisely Capturing Timing Diagrams	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers