Abstract
We study the relationship between two abstraction approaches for pointer programs, Separation Logic and hyperedge replacement grammars. Both employ inductively defined predicates and replacement rules, respectively, for representing (dynamic) data structures, involving abstraction and concretisation operations for symbolic execution. In the Separation Logic case, automatically generating a complete set of such operations requires certain properties of predicates, which are currently implicitly described and manually established. In contrast, the structural properties that guarantee correctness of grammar abstraction are decidable and automatable. Using a property-preserving translation we argue that it is exactly the logic counterparts of those properties that ensure the direct applicability of predicate definitions for symbolic execution.
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.
References
Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005)
Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)
Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL, pp. 259–270. ACM (2005)
Distefano, D., Parkinson, M.J.: jStar: Towards practical verification for Java. ACM Sigplan Notices 43(10), 213–226 (2008)
Dodds, M.: Graph Transformation and Pointer Structures. PhD thesis, The University of York, Department of Computer Science (2008)
Dodds, M., Plump, D.: From hyperedge replacement to separation logic and back. ECEASST 16 (2008)
Dudka, K., Peringer, P., Vojnar, T.: Predator: A practical tool for checking manipulation of dynamic data structures using logic. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 372–378. Springer, Heidelberg (2011)
Fradet, P., Caugne, R., Métayer, D.L.: Static detection of pointer errors: An axiomatisation and a checking algorithm. In: Riis Nielson, H. (ed.) ESOP 1996. LNCS, vol. 1058, pp. 125–140. Springer, Heidelberg (1996)
Haack, C., Hurlin, C.: Separation logic contracts for a Java-like language with fork/join. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 199–215. Springer, Heidelberg (2008)
Heinen, J., Noll, T., Rieger, S.: Juggrnaut: Graph grammar abstraction for unbounded heap structures. In: Proc. 3rd Int. Workshop on Harnessing Theories for Tool Support in Software. ENTCS, vol. 266, pp. 93–107. Elsevier (2010)
Jansen, C., Göbe, F., Noll, T.: Generating inductive predicates for symbolic execution of pointer-manipulating programs. Technical Report AIB 2014-08, RWTH Aachen University, Germany (May 2014), http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2014/2014-08.pdf
Jansen, C., Heinen, J., Katoen, J.-P., Noll, T.: A local Greibach normal form for hyperedge replacement grammars. In: Dediu, A.-H., Inenaga, S., Martín-Vide, C. (eds.) LATA 2011. LNCS, vol. 6638, pp. 323–335. Springer, Heidelberg (2011)
Jeltsch, E., Kreowski, H.-J.: Grammatical inference based on hyperedge replacement. In: Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) Graph Grammars 1990. LNCS, vol. 532, pp. 461–474. Springer, Heidelberg (1990)
Lee, O., Yang, H., Yi, K.: Automatic verification of pointer programs using grammar-based shape analysis. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 124–140. Springer, Heidelberg (2005)
Nellen, J.: Konfluenzanalyse und Vervollstndigung von Graphersetzungssystemen. Master’s thesis, RWTH Aachen University (2010)
Newman, M.: On theories with a combinatorial definition of “equivalence”. Annals of Mathematics 43(2), 223–243 (1942)
Plump, D.: Checking graph-transformation systems for confluence. ECEASST 26 (2010)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. 17th IEEE Symp. on Logic in Computer Science, pp. 55–74. IEEE (2002)
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
Jansen, C., Göbe, F., Noll, T. (2014). Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs. In: Giese, H., König, B. (eds) Graph Transformation. ICGT 2014. Lecture Notes in Computer Science, vol 8571. Springer, Cham. https://doi.org/10.1007/978-3-319-09108-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-09108-2_5
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-09107-5
Online ISBN: 978-3-319-09108-2
eBook Packages: Computer ScienceComputer Science (R0)