SDSAT: Tight integration of small domain encoding and lazy approaches in a separation logic solver

Malay K. Ganai, Muralidhar Talupur, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationTools 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
Pages135-150
Number of pages16
DOIs
StatePublished - Jul 14 2006
Externally publishedYes
Event12th 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 - Vienna, Austria
Duration: Mar 25 2006Apr 2 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3920 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other12th 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
CountryAustria
CityVienna
Period3/25/064/2/06

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'SDSAT: Tight integration of small domain encoding and lazy approaches in a separation logic solver'. Together they form a unique fingerprint.

  • Cite this

    Ganai, M. K., Talupur, M., & Gupta, A. (2006). SDSAT: Tight integration of small domain encoding and lazy approaches in a separation logic solver. In 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 (pp. 135-150). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3920 LNCS). https://doi.org/10.1007/11691372_9