Abstract
We introduce a segment-offset-plane memory model for symbolic execution that supports symbolic pointers, allocations of memory blocks of symbolic sizes, and multi-writes. We further describe our efficient implementation of the model in a free open-source project Bugst. Experimental results provide empirical evidence that the implemented memory model effectively tackles the variable storage-referencing problem of symbolic execution.
The authors have been supported by The Czech Science Foundation, grant GBP202/12/G061.
This is a preview of subscription content, log in via an institution to check access.
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
Beyer, D.: Second competition on software verification. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 594–609. Springer, Heidelberg (2013)
Boyer, R.S., Elspas, B., Levitt, K.N.: SELECT – A formal system for testing and debugging programs by symbolic execution. In: ICRS, pp. 234–245. ACM (1975)
Cadar, C., Dunbar, D., Engler, D.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209–224. USENIX Association (2008)
Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: Automatically generating inputs of death. In: CCS, pp. 322–335. ACM (2006)
Deng, X., Lee, J.: Robby. Efficient and formal generalized symbolic execution. Autom. Softw. Eng. 19(3), 233–301 (2012)
Elkarablieh, B., Godefroid, P., Levin, M.Y.: Precise pointer reasoning for dynamic test generation. In: ISSTA, pp. 129–140. ACM (2009)
Howden, W.E.: Symbolic testing and the DISSECT symbolic evaluation system. IEEE Trans. Software Eng. 3, 266–278 (1977)
Khurshid, S., Păsăreanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003)
King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)
Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: ESEC/FSE, pp. 263–272. ACM (2005)
Slaby, J., Strejček, J., Trtík, M.: Compact symbolic execution. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 193–207. Springer, Heidelberg (2013)
Vanoverberghe, D., Tillmann, N., Piessens, F.: Test input generation for programs with pointers. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 277–291. Springer, Heidelberg (2009)
Xu, Z., Zhang, J.: A test data generation tool for unit testing of C programs. In: QSIC, pp. 107–116. IEEE (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Trtík, M., Strejček, J. (2014). Symbolic Memory with Pointers. In: Cassez, F., Raskin, JF. (eds) Automated Technology for Verification and Analysis. ATVA 2014. Lecture Notes in Computer Science, vol 8837. Springer, Cham. https://doi.org/10.1007/978-3-319-11936-6_27
Download citation
DOI: https://doi.org/10.1007/978-3-319-11936-6_27
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11935-9
Online ISBN: 978-3-319-11936-6
eBook Packages: Computer ScienceComputer Science (R0)
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.