×

Speeding up the constraint-based method in difference logic. (English) Zbl 1475.68076

Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9710, 284-301 (2016).
Summary: Over the years the constraint-based method has been successfully applied to a wide range of problems in program analysis, from invariant generation to termination and non-termination proving. Quite often the semantics of the program under study as well as the properties to be generated belong to difference logic, i.e., the fragment of linear arithmetic where atoms are inequalities of the form \(u - v \leq k\). However, so far constraint-based techniques have not exploited this fact: in general, Farkas’ lemma is used to produce the constraints over template unknowns, which leads to non-linear SMT problems. Based on classical results of graph theory, in this paper we propose new encodings for generating these constraints when program semantics and templates belong to difference logic. Thanks to this approach, instead of a heavyweight non-linear arithmetic solver, a much cheaper SMT solver for difference logic or linear integer arithmetic can be employed for solving the resulting constraints. We present encouraging experimental results that show the high impact of the proposed techniques on the performance of the VeryMax verification system.
For the entire collection see [Zbl 1337.68009].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
68Q60 Specification and verification (program logics, model checking, etc.)
68R07 Computational aspects of satisfiability

Software:

OptiMathSAT; vZ
PDF BibTeX XML Cite
Full Text: DOI Link

References:

[1] Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003) · Zbl 1278.68164
[2] Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Petri net analysis using invariant generation. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 682–701. Springer, Heidelberg (2004) · Zbl 1274.68253
[3] Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Formal Methods Syst. Des. 32(1), 25–55 (2008) · Zbl 1133.68365
[4] Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 378–394. Springer, Heidelberg (2007) · Zbl 1132.68333
[5] Larraz, D., Rodríguez-Carbonell, E., Rubio, A.: SMT-based array invariant generation. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 169–188. Springer, Heidelberg (2013) · Zbl 1426.68056
[6] Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004) · Zbl 1202.68109
[7] Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving termination of imperative programs using Max-SMT. In: Proceeding FMCAD 2013, pp. 218–225. IEEE (2013)
[8] Larraz, D., Nimkar, K., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving non-termination using Max-SMT. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 779–796. Springer, Heidelberg (2014) · Zbl 06349548
[9] Borralleras, C., Lucas, S., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: SAT modulo linear arithmetic for solving polynomial constraints. Journal of Automated Reasoning 48(1), 107–131 (2012) · Zbl 1243.68210
[10] Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339–354. Springer, Heidelberg (2012) · Zbl 1358.68257
[11] Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Minimal-model-guided approaches to solving polynomial constraints and extensions. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 333–350. Springer, Heidelberg (2014) · Zbl 1423.68457
[12] Cousot, P., Cousot, R.: Abstract interpretation : a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Proceeding POPL 1977, pp. 238–252. ACM Press (1977)
[13] Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceeding POPL 1978, pp. 84–96. ACM Press (1978)
[14] Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceeding 2nd International Symposium on Programming, pp. 106–130 (1976) · Zbl 0393.68080
[15] Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001) · Zbl 0984.68034
[16] Miné, A.: The octagon abstract domain. High. Order Symbolic Comput. 19(1), 31–100 (2006) · Zbl 1105.68069
[17] Menasche, M., Berthomieu, B.: Time petri nets for analyzing and verifying time dependent communication protocols. In: Protocol Specification, Testing, and Verification, pp. 161–172 (1983)
[18] Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1989)
[19] Yovine, S.: Model checking timed automata. In: Lectures on Embedded Systems, European Educational Forum, School on Embedded Systems. vol. 1494. LNCS, pp. 114–152. Springer, Heidelberg (1996)
[20] Brockschmidt, M., Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Compositional safety verification with Max-SMT. In: Proceeding FMCAD 2015, pp. 33–40. IEEE (2015)
[21] Kapur, D., Zhang, Z., Horbach, M., Zhao, H., Lu, Q., Nguyen, T.V.: Geometric quantifier elimination heuristics for automatically generating octagonal and max-plus invariants. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 189–228. Springer, Heidelberg (2013) · Zbl 1385.68013
[22] Monniaux, D.: Automatic modular abstractions for linear constraints. In: Proceeding POPL 2009, pp. 140–151. ACM (2009) · Zbl 1315.68102
[23] Lahiri, S.K., Musuvathi, M.: An efficient decision procedure for UTVPI constraints. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 168–183. Springer, Heidelberg (2005) · Zbl 1171.68715
[24] Monniaux, D.: A quantifier elimination algorithm for linear real arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 243–257. Springer, Heidelberg (2008) · Zbl 1182.68213
[25] Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Amsterdam (1998) · Zbl 0970.90052
[26] Dechter, R., Meiri, I., Pearl, J.: Temporal constraint networks. Artif. Intell. 49(1–3), 61–95 (1991) · Zbl 0737.68070
[27] Cormen, T.H., Stein, C., Rivest, R.L., Leiserson, C.E.: Introduction to Algorithms, 2nd edn. McGraw-Hill Higher Education, New York (2001) · Zbl 1047.68161
[28] Frisch, A.M., Peugniez, T.J., Doggett, A.J., Nightingale, P.W.: Solving non-boolean satisfiability problems with stochastic local search: a comparison of encodings. J. Autom. Reasoning 35(1–3), 143–179 (2005) · Zbl 1109.68109
[29] Argelich, J., Manyà, F.: Solving over-constrained problems with SAT technology. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 1–15. Springer, Heidelberg (2005) · Zbl 1124.68430
[30] Press, W.H., Teukolsky, S.A., Vetterling, W.T., Flannery, B.P.: Numerical Recipes: The Art of Scientific Computing. Cambridge Univ. Press, NewYork (1989) · Zbl 0698.65001
[31] Marques-Silva, J., Argelich, J., Graça, A., Lynce, I.: Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell. 62(3–4), 317–343 (2011) · Zbl 1242.90199
[32] Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 447–454. Springer, Heidelberg (2015) · Zbl 06845674
[33] Bjørner, N., Phan, A.-D., Fleckenstein, L.: \[ {\nu }z \] - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194–199. Springer, Heidelberg (2015)
[34] Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: The Barcelogic SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 294–298. Springer, Heidelberg (2008) · Zbl 05301117
[35] Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156–169. Springer, Heidelberg (2006) · Zbl 1187.68558
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.