Similar articles

Abstract: satisfiability modulo theories (SMT) play a key role in verification applications. A crucial SMT problem is to combine separate theory solvers for the union of theories. In previous work, the simplex method is used to determine the solvability of constraint systems and the equalities implied by constraint systems are detected by a multitude of applications of the dual simplex method. We present an effective simplex tableau-based method to identify all implicit equalities such that the simplex method is harnessed to an irreducible minimum. Experimental results show that the method is feasible and effective.

[1] Barrett, C., Berezin, S., 2004. CVC Lite: a new implementation of the cooperating validity checker. LNCS, 3114:515-518.

[2] Barrett, C., Dill, D., Levitt, J., 1996. Validity checking for combinations of theories with equality. LNCS, 1166:187-201.

[3] Barrett, C., de Moura, L., Stump, A., 2005. SMT-COMP: satisfiability modulo theories competition. LNCS, 3576:20-23.

[4] Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P.V., Schulz, S., Sebastiani, R., 2005. The MathSAT 3 System. LNCS, 3632:315-321.

[5] Chvatal, V., 1983. Linear Programming. Springer-Verlag New York, LLC, p.34-45.

[6] Dantzig, G.B., 1973. Fourier-Motzkin elimination and its dual. J. Comb. Theory Ser. A, 14(3):288-297.

[7] Detlefs, D., Nelson, G., Saxe, J.B., 2005. Simplify: a theorem prover for program checking. J. ACM, 52(3):365-473.

[8] Dutertre, B., de Moura, L., 2006. A fast linear-arithmetic solver for DPLL(T). LNCS, 4144:81-94.

[9] Filliatre, J.C., Owre, S., Rueb, H., Shankar, N., 2001. ICS: Integrated Canonization and Solving. Int. Conf. on Computer Aided Verification, p.246-249.

[10] Kroening, D., Strichman, O., 2008. Decision Procedures: An Algorithmic Point of View. Springer-Verlag New York Inc., p.113-122.

[11] Lassez, J.L., McAloon, K., 1992. A canonical form for generalized linear constraints. J. Symb. Comput., 13(1):1-24.

[12] McMillan, K.L., 2004. An Interpolating Theorem Prover. TACAS 2004: Tools and Algorithms for Construction and Analysis of Systems, p.102-121.

[13] Nelson, G., 1981. Techniques for Program Verification. Technical Report, CSL-81-10, Xerox Palo Alto Research Center, Palo Alto, CA.

[14] Nieuwenhuis, R., Oliveras, A., 2005. DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. Int. Conf. on Computer Aided Verification, p.321-324.

[15] Refalo, P., 1998. Approaches to the Incremental Detection of Implicit Equalities with the Revised Simplex Method. Proc. 10th Int. Symp. on Principles of Declarative Programming, p.481-496.

[16] Rueß, H., Shankar, N., 2004. Solving Linear Arithmetic Constraints. Technical Report, CSL-SRI-04-01, SRI International, Menlo Park, CA, USA.

[17] Sheini, H.M., Sakallah, K.A., 2005. A scalable method for solving satisfiability of integer linear arithmetic logic. LNCS, 3569:241-256.

[18] Stuckey, P.J., 1991. Incremental linear constraint solving and detection of implicit equalities. ORSA J. Comput., 3(4):269-271.

[19] Stump, A., Barrett, C.W., Dill, D.L., 2002. CVC: a cooperating validity checker. LNCS, 2404:500-504.

[20] Vanderbei, R.J., 2001. Linear Programming: Foundations and Extensions (2nd Ed.). Springer-Verlag New York, LLC, p.16-22.

[21] Wang, C., Ivancic, F., Ganai, M., Gupta, A., 2005. Deciding separation logic formulae by SAT and incremental negative cycle elimination. LNCS, 3835:322-336.