Verifying Array Manipulating Programs with Full-Program Induction
39
19. Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Proc. of CAV. pp.
193–206 (2007)
20. Knobe, K., Sarkar, V.: Array SSA form and its use in parallelization. In: Proc. of
POPL. pp. 107–120 (1998)
21. Komuravelli, A., Bjorner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using Horn clauses over integers and arrays. In:
Proc. of FMCAD. pp. 89–96 (2015)
22. Lattner, C.: LLVM and Clang: Next generation compiler technology. In: The BSD
Conference. pp. 1–2 (2008)
23. Liu, J., Rival, X.: Abstraction of arrays based on non contiguous partitions. In:
Proc. of VMCAI. pp. 282–299 (2015)
24. Monniaux, D., Gonnord, L.: Cell Morphing: From array programs to array-free
horn clauses. In: Proc. of SAS. pp. 361–382 (2016)
25. de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Proc. of TACAS. pp.
337–340 (2008)
26. Rajkhowa, P., Lin, F.: Extending VIAP to handle array programs. In: Proc. of
VSTTE. pp. 38–49 (2018)
27. Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant
computations. In: Proc. of POPL. pp. 12–27 (1988)
28. Seghir, M.N., Brain, M.: Simplifying the verification of quantified array assertions
via code transformation. In: Proc. of LOPSTR. pp. 194–212 (2012)
29. Sheeran, M., Singh, S., St˚ almarck, G.: Checking safety properties using induction
and a SAT-solver. In: Proc. of FMCAD. pp. 127–144 (2000)
30. Srivastava, S., Gulwani, S.: Program verification using templates over predicate
abstraction. ACM Sigplan Notices 44(6), 223–234 (2009)
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and the
source, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in the chapter’s
Creative Commons license, unless indicated otherwise in a credit line to the material. If
material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need
to obtain permission directly from the copyright holder.
39
19. Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Proc. of CAV. pp.
193–206 (2007)
20. Knobe, K., Sarkar, V.: Array SSA form and its use in parallelization. In: Proc. of
POPL. pp. 107–120 (1998)
21. Komuravelli, A., Bjorner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using Horn clauses over integers and arrays. In:
Proc. of FMCAD. pp. 89–96 (2015)
22. Lattner, C.: LLVM and Clang: Next generation compiler technology. In: The BSD
Conference. pp. 1–2 (2008)
23. Liu, J., Rival, X.: Abstraction of arrays based on non contiguous partitions. In:
Proc. of VMCAI. pp. 282–299 (2015)
24. Monniaux, D., Gonnord, L.: Cell Morphing: From array programs to array-free
horn clauses. In: Proc. of SAS. pp. 361–382 (2016)
25. de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Proc. of TACAS. pp.
337–340 (2008)
26. Rajkhowa, P., Lin, F.: Extending VIAP to handle array programs. In: Proc. of
VSTTE. pp. 38–49 (2018)
27. Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant
computations. In: Proc. of POPL. pp. 12–27 (1988)
28. Seghir, M.N., Brain, M.: Simplifying the verification of quantified array assertions
via code transformation. In: Proc. of LOPSTR. pp. 194–212 (2012)
29. Sheeran, M., Singh, S., St˚ almarck, G.: Checking safety properties using induction
and a SAT-solver. In: Proc. of FMCAD. pp. 127–144 (2000)
30. Srivastava, S., Gulwani, S.: Program verification using templates over predicate
abstraction. ACM Sigplan Notices 44(6), 223–234 (2009)
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and the
source, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in the chapter’s
Creative Commons license, unless indicated otherwise in a credit line to the material. If
material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need
to obtain permission directly from the copyright holder.