 |
 |
 |
 |
 |
 |
 |
|
|
|
| THURSDAY, June 16, 2005, 10:30 AM - 12:00 PM | Room: 208AB | ||
|
TOPIC AREA: LOGIC DESIGN AND TEST (tools) | ||
| SESSION 45 | |||
| SAT: Cool Algorithms and Hot Applications | |||
| Chair: Carl Pixley - Synopsys, Inc., Hillsboro, OR | |||
| Organizers: Harry Foster, Rajeev Ranjan | |||
| Recent advances in SAT have taken formal verification capabilities to a new level. The first paper shows a novel method for extending SAT techniques for liveness properties. The next two papers describe advanced learning techniques. The last paper improves the performance of abstraction refinement for property checking. | |||
 45.1 |
Beyond Safety: Customized SAT-based Model Checking |
||
| Speaker(s): | Malay Ganai - NEC-Labs America, Inc., Princeton, NJ | ||
| Author(s): | Malay Ganai - NEC-Labs America, Inc., Princeton, NJ Aarti Gupta - NEC-Labs America, Inc., Princeton, NJ Pranav Ashar - Real Intent Inc., Santa Clara, CA | ||
| 45.2 | Efficient SAT Solving: Beyond Supercubes | ||
| Speaker(s): | Alan J. Hu - Univ. of British Columbia, Vancouver, BC, Canada | ||
| Author(s): | Domagoj Babic - Univ. of British Columbia, Vancouver, BC, Canada Jesse D. Bingham - Univ. of British Columbia, Vancouver, BC, Canada Alan J. Hu - Univ. of British Columbia, Vancouver, BC, Canada | ||
| 45.3s | Prime Clauses for Fast Enumeration of Satisfying Assignments to Boolean Circuits | ||
| Speaker(s): | Hoonsang Jin - Univ. of Colorado, Boulder, CO | ||
| Author(s): | Hoonsang Jin - Univ. of Colorado, Boulder, CO Fabio Somenzi - Univ. of Colorado, Boulder, CO | ||
| 45.4s | Dynamic Abstraction Using SAT-based BMC | ||
| Speaker(s): | Liang Zhang - Cadence Design Systems, Inc., San Jose, CA | ||
| Author(s): | Liang Zhang - Cadence Design Systems, Inc., San Jose, CA Mukul R. Prasad - Fujitsu Labs Ltd., Sunnyvale, CA Michael S. Hsiao - Virginia Polytechnic Inst., Blacksburg, VA Thomas Sidle - Fujitsu Labs Ltd., Sunnyvale, CA | ||
 | |||