On the Monniaux problem in abstract interpretation. (English) Zbl 1539.68063
Chang, Bor-Yuh Evan (ed.), Static analysis. 26th international symposium, SAS 2019, Porto, Portugal, October 8–11, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11822, 162-180 (2019).
Summary: The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program \(P\), a safety (e.g., non-reachability) specification \(\varphi \), and an abstract domain of invariants \(\mathcal{D} \), does there exist an inductive invariant \(\mathcal{I}\) in \(\mathcal{D}\) guaranteeing that program \(P\) meets its specification \(\varphi \). The Monniaux Problem is of course parameterised by the classes of programs and invariant domains that one considers.
In this paper, we show that the Monniaux Problem is undecidable for unguarded affine programs and semilinear invariants (unions of polyhedra). Moreover, we show that decidability is recovered in the important special case of simple linear loops.
For the entire collection see [Zbl 1425.68008].
In this paper, we show that the Monniaux Problem is undecidable for unguarded affine programs and semilinear invariants (unions of polyhedra). Moreover, we show that decidability is recovered in the important special case of simple linear loops.
For the entire collection see [Zbl 1425.68008].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Almagor, S., Chistikov, D., Ouaknine, J., Worrell, J.: O-minimal invariants for linear loops. In: Proceedings of ICALP. LIPIcs, vol. 107, pp. 114:1-114:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018) · Zbl 1499.68066 |
| [2] | Bakhirkin, A., Monniaux, D.: Extending constraint-only representation of polyhedra with boolean constraints. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 127-145. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99725-4_10 · Zbl 1511.68066 |
| [3] | Cai, J.-Y.: Computing Jordan normal forms exactly for commuting matrices in polynomial time. Technical report, SUNY at Buffalo (2000) |
| [4] | Cai, J.-Y., Lipton, R.J., Zalcstein, Y.: The complexity of the A B C problem. SIAM J. Comput. 29(6), 1878-1888 (2000) · Zbl 0967.20029 |
| [5] | Clarisó, R., Cortadella, J.: The octahedron abstract domain. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 312-327. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27864-1_23 · Zbl 1104.68410 |
| [6] | Cohen, H.: A Course in Computational Algebraic Number Theory. Springer-Verlag, Heidelberg (1993). https://doi.org/10.1007/978-3-662-02945-9 · Zbl 0786.11071 |
| [7] | Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Why does Astrée scale up? Formal Meth. Syst. Des. 35(3), 229-264 (2009) · Zbl 1185.68241 |
| [8] | Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of POPL, pp. 84-96. ACM Press (1978) |
| [9] | Fijalkow, N., Lefaucheux, E., Ohlmann, P., Ouaknine, J., Pouly, A., Worrell, J.: On the monniaux problem in abstract interpretation. CoRR, abs/1907.08257 (2019) |
| [10] | Fijalkow, N., Ohlmann, P., Ouaknine, J., Pouly, A., Worrell, J.: Semialgebraic invariant synthesis for the Kannan-Lipton Orbit Problem. In: Proceedings of STACS. LIPIcs, vol. 66, pp. 29:1-29:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017) · Zbl 1434.37008 |
| [11] | Fijalkow, N., Ohlmann, P., Ouaknine, J., Pouly, A., Worrell, J.: Complete semialgebraic invariant synthesis for the Kannan-LiptonOrbit Problem. Theory of Computing Systems (2019) · Zbl 1461.37028 |
| [12] | Ghorbal, K., Ivančić, F., Balakrishnan, G., Maeda, N., Gupta, A.: Donut domains: efficient non-convex domains for abstract interpretation. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 235-250. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27940-9_16 · Zbl 1326.68094 |
| [13] | Giacobazzi, R., Logozzo, F., Ranzato, F.: Analyzing program analyses. In: Proceedings POPL, pp. 261-273. ACM (2015) · Zbl 1345.68106 |
| [14] | Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361-416 (2000) · Zbl 1133.68370 |
| [15] | Halava, V., Harju, T.: Undecidability of infinite Post correspondence problem for instances of size 9. RAIRO - Theoret. Inf. Appl. Informatique Théorique Appl. 40(4), 551-557 (2006) · Zbl 1114.03035 |
| [16] | Hrushovski, E., Ouaknine, J., Pouly, A., Worrell, J.: Polynomial invariants for affine programs. In: Proceedings of LICS, pp. 530-539. ACM (2018) · Zbl 1497.68113 |
| [17] | Kannan, R., Lipton, R.J.: The Orbit Problem is decidable. In: Proceedings of STOC, pp. 252-261 (1980) |
| [18] | Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the Orbit Problem. J. ACM 33(4), 808-821 (1986) · Zbl 1326.68162 |
| [19] | Karr, M.: Affine relationships among variables of a program. Acta Inf. 6, 133-151 (1976) · Zbl 0358.68025 |
| [20] | Kincaid, Z., Cyphert, J., Breck, J., Reps, T.W.: Non-linear reasoning for invariant synthesis. PACMPL 2(POPL), 54:1-54:33 (2018) |
| [21] | Miné, A.: The octagon abstract domain. In: Proceedings of WCRE, p. 310. IEEE Computer Society (2001) |
| [22] | Monniaux, D.: On the decidability of the existence of polyhedral invariants in transition systems. CoRR, abs/1709.04382 (2017) |
| [23] | Monniaux, D.: On the decidability of the existence of polyhedral invariants in transition systems. Acta Inf. 56(4), 385-389 (2019) · Zbl 1421.68097 |
| [24] | Müller-Olm, M., Seidl, H.: A note on Karr’s Algorithm. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1016-1028. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27836-8_85 |
| [25] | 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). https://doi.org/10.1007/978-3-540-30579-8_2 · Zbl 1111.68514 |
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.
