Abstract
The theory of arrays is widely used in program analysis, (deductive) software verification, bounded model checking, and symbolic execution to model arrays in programs or the computer’s main memory. Nonetheless, the theory as introduced by McCarthy is not expressive enough in many cases since it only supports array updates at single locations. In programs, memory is often modified at multiple locations at once using functions such as memset or memcpy. Furthermore, initialization loops that store loop-counter-dependent values in an array are commonly used. This paper presents an extension of the theory of arrays with λ-terms which makes it possible to reason about such cases. We also discuss how loops can be automatically summarized using such λ-terms.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. IC 183(2), 140–164 (2003)
Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)
Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2006)
Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174–177. Springer, Heidelberg (2009)
Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. JSAT 6, 165–201 (2009)
Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78–92. Springer, Heidelberg (2002)
Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI 2008, pp. 209–224 (2008)
Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: Automatically generating inputs of death. TISSEC 12(2), 10:1–10:38 (2008)
Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)
Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. TSE 38(4), 957–974 (2012)
Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: A software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012)
Falke, S., Merz, F., Sinz, C.: A theory of C-style memory allocation. In: SMT 2011, pp. 71–80 (2011)
Falke, S., Sinz, C., Merz, F.: A theory of arrays with set and copy operations (extended abstract). In: SMT 2012, pp. 97–106 (2012)
Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007)
Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decision procedures for extensions of the theory of arrays. AMAI 50(3-4), 231–254 (2007)
Habermehl, P., Iosif, R., Vojnar, T.: A logic of singly indexed arrays. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 558–573. Springer, Heidelberg (2008)
Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 474–489. Springer, Heidelberg (2008)
Jaffar, J.: Presburger arithmetic with array segments. IPL 12(2), 79–82 (1981)
Kapur, D., Zarba, C.G.: The reduction approach to decision procedures. Tech. Rep. TR-CS-2005-44, Dept. of Computer Science, Univ. of New Mexico (2005)
Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: CGO 2004, pp. 75–88 (2004)
Mateti, P.: A decision procedure for the correctness of a class of programs. JACM 28(2), 215–232 (1981)
McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress 1962, pp. 21–28 (1962)
Merz, F., Falke, S., Sinz, C.: LLBMC: Bounded model checking of C and C++ programs using a compiler IR. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 146–161. Springer, Heidelberg (2012)
de Moura, L.: Answer to Support for AUFBV? on Stack Overflow, http://stackoverflow.com/questions/7411995/support-for-aufbv (2011)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
de Moura, L., Bjørner, N.: Generalized, efficient array decision procedures. In: FMCAD 2009, pp. 45–52 (2009)
Sinz, C., Falke, S., Merz, F.: A precise memory model for low-level bounded model checking. In: SSV 2010 (2010)
Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: LICS 2001, pp. 29–37 (2001)
Suzuki, N., Jefferson, D.: Verification decidability of Presburger array programs. JACM 27(1), 191–205 (1980)
Zhou, M., He, F., Wang, B.Y., Gu, M.: On array theory of bounded elements. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 570–584. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Falke, S., Merz, F., Sinz, C. (2014). Extending the Theory of Arrays: memset, memcpy, and Beyond. In: Cohen, E., Rybalchenko, A. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2013. Lecture Notes in Computer Science, vol 8164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54108-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-54108-7_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54107-0
Online ISBN: 978-3-642-54108-7
eBook Packages: Computer ScienceComputer Science (R0)