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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ackermann, W.: Solvable Cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics (1954)
Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of Timed Automata via Satisfiability Checking. In: Proc. of Formal Techniques in Real-Time and Fault Tolerant Systems (2002)
Adams, J., Balas, E., Zawack, D.: The shifting bottleneck procedure for job shop scheduling. In: Management Science (1988)
Filliatre, J.-C., Owre, S., Rueß, H., Shankar, N.: ICS: Integrated Canonizer and Solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 246. Springer, Heidelberg (2001)
Parthasarathy, G., Iyer, M.K., Cheng, K.-T., Wang, C.: An Efficient Finite-Domain Constraint Solver for RTL Circuits. In: Proceedings of DAC (2004)
Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992)
Kröning, D., Ouaknine, J., Seshia, S.A., Strichman, O.: Abstraction-based satisfiability solving of presburger arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 308–320. Springer, Heidelberg (2004)
Bik, A.J.C., Wijshoff, H.A.G.: Implementation of Fourier-Motzkin Elimination. In: Technical Report 94-42, Dept. of Computer Science, Leiden University (1994)
Zhang, L., Malik, S.: The Quest for Efficient Boolean Satisfiability Solvers. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 17. Springer, Heidelberg (2002)
Pnueli, A., Rodeh, Y., Strichman, O., Siegel, M.: The Small Model Property: How small can it be? Information and computation 178(1), 279–293 (2002)
Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding separation formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 209. Springer, Heidelberg (2002)
Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531. Springer, Heidelberg (1991)
Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A Hybrid SAT-based Decision Procedure for Separation Logic with Uninterpreted Functions. In: Proceedings of DAC (2003)
Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Deciding CLU logic formulas via Boolean and peudo-Boolean encodings. In: Workshop on Constraints in Formal Verification (2002)
Barrett, C., Dill, D.L., Levitt, J.: Validity Checking for Combination of Theories with Equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166. Springer, Heidelberg (1996)
Armando, A., Castellini, C., Giunchiglia, E., Idini, M., Maratea, M.: TSAT++: An Open Platform for Satisfiability Modulo Theories. In: Proceedings of Pragmatics of Decision Procedures in Automated Resonings, PDPAR 2004 (2004)
Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T.A., van Rossum, P., Schulz, S., Sebastiani, R.: An incremental and layered procedure for the satisfiability of linear arithmetic logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 317–333. Springer, Heidelberg (2005)
Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 321–334. Springer, Heidelberg (2005)
Wang, C., Ivancic, F., Ganai, M., Gupta, A.: Deciding Separation Logic Formulae with SAT by Incremental Negative Cycle Elimination. In: Proceeding of Logic for Programming (2005)
Talupur, M., Sinha, N., Strichman, O., Pnueli, A.: Range allocation for separation logic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 148–161. Springer, Heidelberg (2004)
Aloul, F., Ramani, A., Markov, I., Sakallah, K.: PBS: A backtrack search pseudo-Boolean solver. In: Symposium on the Theory and Applications of Satisfiability Testing, SAT (2002)
Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge (1990)
Cotton, S.: Satisfiability Checking with Difference Constraints. In: IMPRS Computer Science, Saarbruceken (2005)
Pratt, V.: Two Easy Theories Whose Combination is Hard, in Technical report, MIT (1977)
Ramalingam, G., Song, J., Joscovicz, L., Miller, R.: Solving difference constraints incrementally. Alogrithmica (1999)
Strichman, O.: http://iew3.techninon.ac.il/~ofers
Hochbaum, D.S.: Approximation Algorithms for NP-hard Problems: PWS Publishing Company (1997)
Cherkassky, B.V., Goldberg, E.: Negative-cycle Detection Algorithms. In: European Symposium on Algorithms (1996)
Moore, R.E.: Interval Analysis. Prentice-Hall, NJ (1966)
Hickey, T., Ju, Q., Emden, H.V.: Interval Arithmetic: from principles to implementation. Journal of the ACM (2001)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of Design Automation Conference (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ganai, M.K., Talupur, M., Gupta, A. (2006). SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver. In: Hermanns, H., Palsberg, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2006. Lecture Notes in Computer Science, vol 3920. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691372_9
Download citation
DOI: https://doi.org/10.1007/11691372_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33056-1
Online ISBN: 978-3-540-33057-8
eBook Packages: Computer ScienceComputer Science (R0)