Abstract
The verification community has studied dynamic data structures primarily in a bottom-up way by analyzing pointers and the shapes induced by them. Recent work in fields such as separation logic has made significant progress in extracting shapes from program source code. Many real world programs however manipulate complex data whose structure and content is most naturally described by formalisms from object oriented programming and databases. In this paper, we look at the verification of programs with dynamic data structures from the perspective of content representation. Our approach is based on description logic, a widely used knowledge representation paradigm which gives a logical underpinning for diverse modeling frameworks such as UML and ER. Technically, we assume that we have separation logic shape invariants obtained from a shape analysis tool, and requirements on the program data in terms of description logic. We show that the two-variable fragment of first order logic with counting and trees can be used as a joint framework to embed suitable fragments of description logic and separation logic.
Kotek, Veith and Zuleger were supported by the Austrian National Research Network S11403-N23 (RiSE) of the Austrian Science Fund (FWF) and by the Vienna Science and Technology Fund (WWTF) through grants PROSEED and ICT12-059. Simkus was supported by the FWF grant P25518 and the WWTF grant ICT12-15.
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
Apel, S., Beyer, D., Friedberger, K., Raimondi, F., von Rhein, A.: Domain types: Abstract-domain selection based on variable usage. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 262–278. Springer, Heidelberg (2013)
Artale, A., Calvanese, D., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: Reasoning over extended ER models. In: Parent, C., Schewe, K.-D., Storey, V.C., Thalheim, B. (eds.) ER 2007. LNCS, vol. 4801, pp. 277–292. Springer, Heidelberg (2007)
Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic handbook: theory, implementation, and applications. Cambridge University Press (2003)
Baader, F., Zarrieß, B.: Verification of golog programs over description logic actions. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 181–196. Springer, Heidelberg (2013)
Banerjee, A., Naumann, D.A., Rosenberg, S.: Local reasoning for global invariants, part I: Region logic. J. ACM 60(3), 18 (2013)
Berardi, D., Calvanese, D., De Giacomo, G.: Reasoning on UML class diagrams. Artificial Intelligence 168(1-2), 70–118 (2005)
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)
Borgida, A.: On the relative expressiveness of description logics and predicate logics. Artif. Intell. 82(1-2), 353–367 (1996)
Calvanese, D., Ortiz, M., Šimkus, M.: Evolving graph databases under description logic constraints. In: Proc. of DL, pp. 120–131 (2013)
Charatonik, W., Witkowski, P.: Two-variable logic with counting and trees. In: LICS, pp. 73–82 (2013)
Chin, W., David, C., Nguyen, H.H., Qin, S.: Enhancing modular oo verification with separation logic. In: POPL, pp. 87–99. ACM (2008)
Demyanova, Y., Veith, H., Zuleger, F.: On the concept of variable roles and its use in software analysis. In: FMCAD, pp. 226–230 (2013)
Georgieva, L., Maier, P.: Description Logics for shape analysis. In: SEFM, pp. 321–331 (2005)
De Giacomo, G., Lespérance, Y., Patrizi, F.: Bounded situation calculus action theories and decidable verification. In: Proc. of KR (2012)
Hawkins, P., Aiken, A., Fisher, K., Rinard, M., Sagiv, M.: Data structure fusion. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 204–221. Springer, Heidelberg (2010)
Holík, L., Lengál, O., Rogalewicz, A., Šimáček, J., Vojnar, T.: Fully automated shape analysis based on forest automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 740–755. Springer, Heidelberg (2013)
Ishtiaq, S.S., O’Hearn, P.W.: Bi as an assertion language for mutable data structures. In: POPL, pp. 14–26. ACM (2001)
James, D., Leonard, T., O’Leary, J., Talupur, M., Tuttle, M.R.: Extracting models from design documents with mapster. In: PODC (2008)
Kotek, T., Simkus, M., Veith, H., Zuleger, F.: Extending alcqio with reachability. CoRR, abs/1402.6804 (2014)
Lutz, C., Wolter, F., Zakharyaschev, M.: Temporal description logics: A survey. In: Proc. of TIME. IEEE Computer Society (2008)
Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: POPL, pp. 611–622. ACM, USA (2011)
W3C OWL Working Group. OWL 2 Web Ontology Language: Document Overview. W3C Recommendation (October 27, 2009)
Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. SIGPLAN Not. 43(1), 75–86 (2008)
Reynolds, J.C.: Separation Logic: A logic for shared mutable data structures. In: Proc. of LICS, pp. 55–74. IEEE Computer Society, Washington, DC (2002)
Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 530–545. Springer, Heidelberg (2004)
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
Calvanese, D., Kotek, T., Šimkus, M., Veith, H., Zuleger, F. (2014). Shape and Content. In: Albert, E., Sekerinski, E. (eds) Integrated Formal Methods. IFM 2014. Lecture Notes in Computer Science(), vol 8739. Springer, Cham. https://doi.org/10.1007/978-3-319-10181-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-10181-1_1
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10180-4
Online ISBN: 978-3-319-10181-1
eBook Packages: Computer ScienceComputer Science (R0)