|
Published Articles >> Table of Contents >> Abstract
40th Design Automation Conference (DAC'03)
p. 425
A Hybrid SAT-Based Decision Procedure for Separation Logic with Uninterpreted Functions
Sanjit A. Seshia, Carnegie Mellon University, Pittsburgh, PA
Shuvendu K. Lahiri, Carnegie Mellon University, Pittsburgh, PA
Randal E. Bryant, Carnegie Mellon University, Pittsburgh, PA
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DAC.2003.1219039
Send link to a friend
| Abstract |
|
SAT-based decision procedures for quantifier-free fragments of first-order logic have proved to be useful in formal verification. These decision procedures are either based on encoding atomic subformulas with Boolean variables, or by encoding integer variables as bit-vectors. Based on evaluating these two encoding methods on a diverse set of hardware and software benchmarks, we conclude that neither method is robust to variations in formula characteristics. We therefore propose a new hybrid technique that combines the two methods. We give experimental results showing that the hybrid method can significantly outperform either approach as well as other decision procedures.
|
 Additional Information
|
Index Terms- Design verification, Decision procedures, Boolean satisfiability, Theorem proving
Citation:
Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant,
"A Hybrid SAT-Based Decision Procedure for Separation Logic with Uninterpreted Functions,"
dac,
p. 425,
40th Design Automation Conference (DAC'03),
2003
|
|
