Improving strategies via SMT solving. (English) Zbl 1326.68093
Barthe, Gilles (ed.), Programming languages and systems. 20th European symposium on programming, ESOP 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19717-8/pbk). Lecture Notes in Computer Science 6602, 236-255 (2011).
Summary: We consider the problem of computing numerical invariants of programs by abstract interpretation. Our method eschews two traditional sources of imprecision: (i) the use of widening operators for enforcing convergence within a finite number of iterations (ii) the use of merge operations (often, convex hulls) at the merge points of the control flow graph. It instead computes the least inductive invariant expressible in the domain at a restricted set of program points, and analyzes the rest of the code en bloc. We emphasize that we compute this inductive invariant precisely. For that we extend the strategy improvement algorithm of T. Gawlitza and H. Seidl [Lect. Notes Comput. Sci. 4646, 23–40 (2007; Zbl 1179.68037)]. If we applied their method directly, we would have to solve an exponentially sized system of abstract semantic equations, resulting in memory exhaustion. Instead, we keep the system implicit and discover strategy improvements using SAT modulo real linear arithmetic (SMT). For evaluating strategies we use linear programming. Our algorithm has low polynomial space complexity and performs for contrived examples in the worst case exponentially many strategy improvement steps; this is unsurprising, since we show that the associated abstract reachability problem is \(\Pi _{2} ^{\mathrm {P}}\)-complete.
For the entire collection see [Zbl 1213.68027].
For the entire collection see [Zbl 1213.68027].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
Citations:
Zbl 1179.68037References:
| [1] | Adjé, A., Gaubert, S., Goubault, E.: Computing the smallest fixed point of nonexpansive mappings arising in game theory and static analysis of programs. ArXiv e-prints (June 2008) · Zbl 1309.47057 |
| [2] | Adjé, A., Gaubert, S., Goubault, E.: Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 23–42. Springer, Heidelberg (2010) · Zbl 1260.68082 · doi:10.1007/978-3-642-11957-6_3 |
| [3] | Ball, T., Jones, R.B. (eds.): CAV 2006. LNCS, vol. 4144. Springer, Heidelberg (2006) · Zbl 1114.68002 |
| [4] | Björklund, H., Sandberg, S., Vorobyov, S.: Optimization on completely unimodal hypercubes. Technichal report 2002-18, Uppsala University (2002) |
| [5] | Bjorklund, H., Sandberg, S., Vorobyov, S.: Complexity of Model Checking by Iterative Improvement: the Pseudo-Boolean Framework. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 381–394. Springer, Heidelberg (2004) · Zbl 1254.68144 · doi:10.1007/978-3-540-39866-0_38 |
| [6] | Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Programming Language Design and Implementation (PLDI), ACM, New York (2003) · Zbl 1026.68514 |
| [7] | Cochet-Terrasson, J., Gaubert, S., Gunawardena, J.: A Constructive Fixed Point Theorem for Min-Max Functions. Dynamics and Stability of Systems 14(4), 407–433 (1999) · Zbl 0958.47028 · doi:10.1080/026811199281967 |
| [8] | Colón, M.A., Sankaranarayanan, S., Sipma, H.: 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 · doi:10.1007/978-3-540-45069-6_39 |
| [9] | Costan, A., Gaubert, S., Goubault, E., Martel, M., Putot, S.: A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 462–475. Springer, Heidelberg (2005) · Zbl 1081.68616 · doi:10.1007/11513988_46 |
| [10] | Cousot, P.: Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005) · Zbl 1111.68503 · doi:10.1007/978-3-540-30579-8_1 |
| [11] | Cousot, P., Cousot, R.: Static Determination of Dynamic Properties of Programs. In: Second Int. Symp. on Programming, Dunod, Paris, France (1976) · Zbl 0393.68080 |
| [12] | Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977) · Zbl 1149.68389 · doi:10.1145/512950.512973 |
| [13] | Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL (1978) · doi:10.1145/512760.512770 |
| [14] | Dutertre, B., de Moura, L.: The Yices SMT solver. Tool paper (August 2006), http://yices.csl.sri.com/tool-paper.pdf |
| [15] | Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for dpll(t). In: Ball, Jones [3] · doi:10.1007/11817963_11 |
| [16] | Gaubert, S., Goubault, E., Taly, A., Zennou, S.: Static analysis by policy iteration on relational domains. In: Nicola [38] · Zbl 1187.68151 · doi:10.1007/978-3-540-71316-6_17 |
| [17] | Gawlitza, T., Seidl, H.: Precise relational invariants through strategy iteration. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 23–40. Springer, Heidelberg (2007) · Zbl 1179.68037 · doi:10.1007/978-3-540-74915-8_6 |
| [18] | Gawlitza, T., Seidl, H.: Precise fixpoint computation through strategy iteration. In: Nicola [38] · Zbl 1187.68152 · doi:10.1007/978-3-540-71316-6_21 |
| [19] | Gawlitza, T., Seidl, H.: Precise interval analysis vs. parity games. In: Cuéllar, J., Maibaum, T.S.E., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 342–357. Springer, Heidelberg (2008) · doi:10.1007/978-3-540-68237-0_24 |
| [20] | Gawlitza, T., Leroux, J., Reineke, J., Seidl, H., Sutre, G., Wilhelm, R.: Polynomial precise interval analysis revisited. In: Albers, S., Alt, H., Näher, S. (eds.) Efficient Algorithms. LNCS, vol. 5760, pp. 422–437. Springer, Heidelberg (2009) · Zbl 1258.65048 · doi:10.1007/978-3-642-03456-5_28 |
| [21] | Gawlitza, T.M., Seidl, H.: Solving systems of rational equations through strategy iteration. Technical report, TUM (2009) · Zbl 1242.68160 |
| [22] | Gawlitza, T.M., Seidl, H.: Computing relaxed abstract semantics w.r.t. quadratic zones precisely. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 271–286. Springer, Heidelberg (2010) · Zbl 1306.68025 · doi:10.1007/978-3-642-15769-1_17 |
| [23] | Gonnord, L.: Accelération abstraite pour l’amélioration de la précision en analyse des relations linéaires. PhD thesis, Université Joseph Fourier (October 2007), http://tel.archives-ouvertes.fr/tel-00196899/en/ |
| [24] | Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 144–160. Springer, Heidelberg (2006) · Zbl 1225.68071 · doi:10.1007/11823230_10 |
| [25] | Gopan, D., Reps, T.W.: Lookahead widening. In: Ball, Jones [3] · doi:10.1007/11817963_41 |
| [26] | Rice, H.G.: Classes of recursively enumerable sets and their decision problems. In: Transactions of the American Mathematical Society, vol. 74. AMS, Providence (1953) · Zbl 0053.00301 · doi:10.1090/S0002-9947-1953-0053041-6 |
| [27] | Halbwachs, N.: Delay analysis in synchronous programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 333–346. Springer, Heidelberg (1993) · doi:10.1007/3-540-56922-7_28 |
| [28] | Hoffman, A., Karp, R.: On Nonterminating Stochastic Games. Management Sci. 12, 359–370 (1966) · Zbl 0136.14303 · doi:10.1287/mnsc.12.5.359 |
| [29] | Howard, R.: Dynamic Programming and Markov Processes. Wiley, NY (1960) · Zbl 0091.16001 |
| [30] | Leconte, J., Roux, S.L., Liberti, L., Marinelli, F.: Code verification by static analysis: a mathematical programming approach. Technical report, LIX, Ecole Polytechnique, Palaiseau (August 2009) · Zbl 1342.68086 |
| [31] | Leroux, J., Sutre, G.: Accelerated data-flow analysis. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 184–199. Springer, Heidelberg (2007) · Zbl 1211.68093 · doi:10.1007/978-3-540-74061-2_12 |
| [32] | Megiddo, N.: On the Complexity of Linear Programming. In: Bewley, T. (ed.) Advances in Economic Theory: 5th World Congress, Cambridge University Press, Cambridge (1987) · Zbl 0735.90044 |
| [33] | 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 · doi:10.1007/3-540-44978-7_10 |
| [34] | Miné, A.: The octagon abstract domain. In: WCRE (2001) · Zbl 1105.68069 · doi:10.1109/WCRE.2001.957836 |
| [35] | Miné, A.: Domaines numériques abstraits faiblement relationnels. PhD thesis, École polytechnique (2004) |
| [36] | 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 · doi:10.1007/978-3-540-89439-1_18 |
| [37] | Monniaux, D.: Automatic modular abstractions for linear constraints. In: Shao, Z., Pierce, B.C. (eds.) POPL, pp. 140–151. ACM, New York (2009) · Zbl 1315.68102 |
| [38] | Nicola, R.D.: Programming Languages and Systems, ESOP 2007. LNCS, vol. 4421. Springer, Heidelberg (2007) · doi:10.1007/978-3-540-71316-6 |
| [39] | Puri, A.: Theory of Hybrid and Discrete Systems. PhD thesis, University of California, Berkeley (1995) |
| [40] | Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994) · Zbl 0829.90134 · doi:10.1002/9780470316887 |
| [41] | Sankaranarayanan, S., Sipma, H., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 53–68. Springer, Heidelberg (2004) · Zbl 1104.68023 · doi:10.1007/978-3-540-27864-1_7 |
| [42] | Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005) · Zbl 1111.68514 · doi:10.1007/978-3-540-30579-8_2 |
| [43] | Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons, Inc., New York (1986) · Zbl 0665.90063 |
| [44] | Stockmeyer, L.J.: The polynomial-time hierarchy. Theoretical Computer Science 3(1), 1–22 (1976) · Zbl 0353.02024 · doi:10.1016/0304-3975(76)90061-X |
| [45] | Vöge, J., Jurdziński, M.: A Discrete Strategy Improvement Algorithm for Solving Parity Games. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 202–215. Springer, Heidelberg (2000) · Zbl 0974.68527 · doi:10.1007/10722167_18 |
| [46] | Wrathall, C.: Complete sets and the polynomial-time hierarchy. Theor. Comput. Sci. 3(1), 23–33 (1976) · Zbl 0366.02031 · doi:10.1016/0304-3975(76)90062-1 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
