A Calculus for Modular Loop Acceleration
75
20. Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: SAS ’06. pp. 144–160. LNCS 4134 (2006).
https://doi.org/10.1007/11823230 10
21. Gonnord, L., Schrammel, P.: Abstract acceleration in linear relation analysis. Science of Computer Programming 93, 125–153 (2014).
https://doi.org/10.1016/j.scico.2013.09.016
22. Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu,
R.: Proving non-termination. In: POPL ’08. pp. 147–158 (2008).
https://doi.org/10.1145/1328438.1328459
23. Hojjat, H., Iosif, R., Konecn´ y, F., Kuncak, V., R¨ ummer, P.: Accelerating interpolants.
In: ATVA ’12. pp. 187–202. LNCS 7561 (2012). https://doi.org/10.1007/978-3-64233386-6 16
24. Hojjat, H., Konecn´ y, F., Garnier, F., Iosif, R., Kuncak, V., R¨ ummer, P.: A verification toolkit for numerical transition systems - tool paper. In: FM ’12. pp. 247–251.
LNCS 7436 (2012). https://doi.org/10.1007/978-3-642-32759-9 21
25. Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: POPL ’14. pp. 529–540 (2014).
https://doi.org/10.1145/2535838.2535843
26. Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.W.: Compositional
recurrence analysis revisited. In: PLDI ’17. pp. 248–262 (2017).
https://doi.org/10.1145/3062341.3062373
27. Konecn´ y, F.: PTIME computation of transitive closures of octagonal relations. In:
TACAS ’16. pp. 645–661. LNCS 9636 (2016). https://doi.org/10.1007/978-3-66249674-9 42
28. Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in
C programs for fast counterexample detection. FMSD 47(1), 75–92 (2015).
https://doi.org/10.1007/s10703-015-0228-1
29. Madhukar, K., Wachter, B., Kroening, D., Lewis, M., Srivas, M.K.: Accelerating invariant generation. In: FMCAD ’15. pp. 105–111 (2015).
https://doi.org/10.1109/FMCAD.2015.7542259
30. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: TACAS ’08. pp. 337–340.
LNCS 4963 (2008). https://doi.org/10.1007/978-3-540-78800-3 24
31. Ouaknine, J., Pinto, J.S., Worrell, J.: On termination of integer linear loops. In:
SODA ’15. pp. 957–969 (2015). https://doi.org/10.1137/1.9781611973730.65
32. Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition
systems. In: CAV ’19. pp. 97–115. LNCS 11562 (2019). https://doi.org/10.1007/9783-030-25543-5 7
33. Strejcek, J., Trt´ ık, M.: Abstracting path conditions. In: ISSTA ’12. pp. 155–165
(2012). https://doi.org/10.1145/2338965.2336772
34. Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: A cross-community infrastructure for logic solving. In: IJCAR ’14. pp. 367–373. LNCS 8562 (2014).
https://doi.org/10.1007/978-3-319-08587-6 28
35. Termination problems data base (TPDB), http://termination-portal.org/wiki/
TPDB
75
20. Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: SAS ’06. pp. 144–160. LNCS 4134 (2006).
https://doi.org/10.1007/11823230 10
21. Gonnord, L., Schrammel, P.: Abstract acceleration in linear relation analysis. Science of Computer Programming 93, 125–153 (2014).
https://doi.org/10.1016/j.scico.2013.09.016
22. Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu,
R.: Proving non-termination. In: POPL ’08. pp. 147–158 (2008).
https://doi.org/10.1145/1328438.1328459
23. Hojjat, H., Iosif, R., Konecn´ y, F., Kuncak, V., R¨ ummer, P.: Accelerating interpolants.
In: ATVA ’12. pp. 187–202. LNCS 7561 (2012). https://doi.org/10.1007/978-3-64233386-6 16
24. Hojjat, H., Konecn´ y, F., Garnier, F., Iosif, R., Kuncak, V., R¨ ummer, P.: A verification toolkit for numerical transition systems - tool paper. In: FM ’12. pp. 247–251.
LNCS 7436 (2012). https://doi.org/10.1007/978-3-642-32759-9 21
25. Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: POPL ’14. pp. 529–540 (2014).
https://doi.org/10.1145/2535838.2535843
26. Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.W.: Compositional
recurrence analysis revisited. In: PLDI ’17. pp. 248–262 (2017).
https://doi.org/10.1145/3062341.3062373
27. Konecn´ y, F.: PTIME computation of transitive closures of octagonal relations. In:
TACAS ’16. pp. 645–661. LNCS 9636 (2016). https://doi.org/10.1007/978-3-66249674-9 42
28. Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in
C programs for fast counterexample detection. FMSD 47(1), 75–92 (2015).
https://doi.org/10.1007/s10703-015-0228-1
29. Madhukar, K., Wachter, B., Kroening, D., Lewis, M., Srivas, M.K.: Accelerating invariant generation. In: FMCAD ’15. pp. 105–111 (2015).
https://doi.org/10.1109/FMCAD.2015.7542259
30. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: TACAS ’08. pp. 337–340.
LNCS 4963 (2008). https://doi.org/10.1007/978-3-540-78800-3 24
31. Ouaknine, J., Pinto, J.S., Worrell, J.: On termination of integer linear loops. In:
SODA ’15. pp. 957–969 (2015). https://doi.org/10.1137/1.9781611973730.65
32. Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition
systems. In: CAV ’19. pp. 97–115. LNCS 11562 (2019). https://doi.org/10.1007/9783-030-25543-5 7
33. Strejcek, J., Trt´ ık, M.: Abstracting path conditions. In: ISSTA ’12. pp. 155–165
(2012). https://doi.org/10.1145/2338965.2336772
34. Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: A cross-community infrastructure for logic solving. In: IJCAR ’14. pp. 367–373. LNCS 8562 (2014).
https://doi.org/10.1007/978-3-319-08587-6 28
35. Termination problems data base (TPDB), http://termination-portal.org/wiki/
TPDB