Name
Title | ||
|---|---|---|
A hybrid SAT-based decision procedure for separation logic with uninterpreted functions |
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. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1145/775832.775945 | DAC |
Keywords | Field | DocType |
atomic subformulas,boolean variable,hybrid method,decision procedure,uninterpreted function,hybrid sat-based decision procedure,encoding method,separation logic,sat-based decision procedure,first-order logic,new hybrid technique,diverse set,algorithms,boolean satisfiability,theorem,theorem proving,measurement,robustness,formal verification,algorithm design and analysis,hardware,boolean variables,integrated circuit design,encoding,first order logic,computer science,logic design | Logic synthesis,Separation logic,Computer science,Automated theorem proving,Boolean satisfiability problem,Algorithm,Robustness (computer science),Theoretical computer science,First-order logic,Boolean data type,Formal verification | Conference |
ISSN | ISBN | Citations |
0738-100X | 1-58113-688-9 | 50 |
PageRank | References | Authors |
2.58 | 13 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sanjit A. Seshia | 1 | 2226 | 168.09 |
| Shuvendu K. Lahiri | 2 | 1424 | 68.18 |
| Randal E. Bryant | 3 | 9204 | 1194.64 |