TY - GEN
T1 - SDSAT
T2 - 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006
AU - Ganai, Malay K.
AU - Talupur, Muralidhar
AU - Gupta, Aarti
PY - 2006
Y1 - 2006
N2 - Existing Separation Logic (a.k.a Difference Logic, DL) solvers can be broadly classified as eager or lazy, each with its own merits and de-merits. We propose a novel Separation Logic Solver SDSAT that combines the strengths of both these approaches and provides a robust performance over a wide set of benchmarks. The solver SDSAT works in two phases: allocation and solve. In the allocation phase, it allocates non-uniform adequate ranges for variables appearing in separation predicates. This phase is similar to previous small domain encoding approaches, but uses a novel algorithm Nu-SMOD with 1-2 orders of magnitude improvement in performance and smaller ranges for variables. Furthermore, the Separation Logic formula is not transformed into an equi-satisfiable Boolean formula in one step, but rather done lazily in the following phase. In the solve phase, SDSAT uses a lazy refinement approach to search for a satisfying model within the allocated ranges. Thus, any partially DL-theory consistent model can be discarded if it can not be satisfied within the allocated ranges. Note the crucial difference: in eager approaches, such a partially consistent model is not allowed in the first place, while in lazy approaches such a model is never discarded. Moreover, we dynamically refine the allocated ranges and search for a feasible solution within the updated ranges. This combined approach benefits from both the smaller search space (as in eager approaches) and also from the theory-specific graph-based algorithms (characteristic of lazy approaches). Experimental results show that our method is robust and always better than or comparable to state-of-the art solvers.
AB - Existing Separation Logic (a.k.a Difference Logic, DL) solvers can be broadly classified as eager or lazy, each with its own merits and de-merits. We propose a novel Separation Logic Solver SDSAT that combines the strengths of both these approaches and provides a robust performance over a wide set of benchmarks. The solver SDSAT works in two phases: allocation and solve. In the allocation phase, it allocates non-uniform adequate ranges for variables appearing in separation predicates. This phase is similar to previous small domain encoding approaches, but uses a novel algorithm Nu-SMOD with 1-2 orders of magnitude improvement in performance and smaller ranges for variables. Furthermore, the Separation Logic formula is not transformed into an equi-satisfiable Boolean formula in one step, but rather done lazily in the following phase. In the solve phase, SDSAT uses a lazy refinement approach to search for a satisfying model within the allocated ranges. Thus, any partially DL-theory consistent model can be discarded if it can not be satisfied within the allocated ranges. Note the crucial difference: in eager approaches, such a partially consistent model is not allowed in the first place, while in lazy approaches such a model is never discarded. Moreover, we dynamically refine the allocated ranges and search for a feasible solution within the updated ranges. This combined approach benefits from both the smaller search space (as in eager approaches) and also from the theory-specific graph-based algorithms (characteristic of lazy approaches). Experimental results show that our method is robust and always better than or comparable to state-of-the art solvers.
UR - http://www.scopus.com/inward/record.url?scp=33745787729&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33745787729&partnerID=8YFLogxK
U2 - 10.1007/11691372_9
DO - 10.1007/11691372_9
M3 - Conference contribution
AN - SCOPUS:33745787729
SN - 3540330569
SN - 9783540330561
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 135
EP - 150
BT - Tools and Algorithms for the Construction and Analysis of Systems - 12th International Conference, TACAS 2006. Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2006
Y2 - 25 March 2006 through 2 April 2006
ER -