Navegar

Colección

Datos Estadísticas

Artículo

Garbervetsky, D.; Gorín, D.; Neisen, A. "Enforcing structural invariants using dynamic frames" (2011) 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011. 6605 LNCS:65-80
Este artículo es de Acceso Abierto y puede ser descargado en su versión final desde nuestro repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

The theory of dynamic frames is a promising approach to handle the so-called framing problem, that is, giving a precise characterizations of the locations in the heap that a procedure may modify. In this paper, we show that the machinery used for dynamic frames may be exploited even further. In particular, we use it to check that implementations of abstract data types maintain certain structural invariants that are very hard to express with usual means, including being acyclic (like non-circular linked lists and trees) and having a unique path between nodes (like in a tree). The idea is that regions in this formalism over-approximate the set of reachable objects. We can then maintain this structural invariants by including special preconditions in assignments, of the kind that can be verified by state-of-the-art SMT-based tools. To test this approach we modified the verifier for the Dafny programming language in a suitable way and were able to enforce these invariants in non-trivial examples. © 2011 Springer-Verlag.

Registro:

Documento: Artículo
Título:Enforcing structural invariants using dynamic frames
Autor:Garbervetsky, D.; Gorín, D.; Neisen, A.
Ciudad:Saarbrucken
Filiación:Departamento de Computación, FCEyN, Universidad de Buenos Aires, Argentina
Palabras clave:Abstract data types; Dynamic frame; Non-circular; Non-trivial; Programming language; Structural invariants; Theory of dynamics; Algorithms; Machinery; Trees (mathematics)
Año:2011
Volumen:6605 LNCS
Página de inicio:65
Página de fin:80
DOI: http://dx.doi.org/10.1007/978-3-642-19835-9_8
Título revista:17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
PDF:https://bibliotecadigital.exactas.uba.ar/download/paper/paper_03029743_v6605LNCS_n_p65_Garbervetsky.pdf
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v6605LNCS_n_p65_Garbervetsky

Referencias:

  • Barnett, M., Leino, K.R.M., Schulte, W., The spec# programming system: An overview (2005) LNCS, 3362, pp. 49-69. , Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. Springer, Heidelberg
  • Clarke, D., Potter, J., Noble, J., Ownership types for flexible alias protection (1998) Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 1998), pp. 48-64. , ACM Press, New York
  • Huizing, K., Kuiper, R., Verification of object oriented programs using class invariants (2000) LNCS, 1783, pp. 208-221. , FASE 2000. Springer, Heidelberg
  • Jacobs, B., Smans, J., Piessens, F., VeriFast: Imperative Programs as Proofs VSTTE Workshop on Tools & Experiments (2010)
  • Kassios, I.T., The dynamic frames theory (2010) Formal Aspects of Computing
  • Lahiri, S., Qadeer, S., Verifying properties of well-founded linked lists (2006) Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2006), pp. 115-126. , ACM Press, New York
  • Leino, K.R.M., Dafny: An automatic program verifier for functional correctness (2010) LNCS, 6355, pp. 348-370. , Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. Springer, Heidelberg
  • Leino, K.R.M., Müller, P., A basis for verifying multi-threaded programs (2009) LNCS, 5502, pp. 378-393. , Castagna, G. (ed.) ESOP 2009. Springer, Heidelberg
  • Leino, K.R.M., Nelson, G., Data abstraction and information hiding (2002) ACM TOPLAS, 24 (5), pp. 491-553
  • Lev-Ami, T., Immerman, N., Reps, T., Sagiv, M., Srivastava, S., Yorsh, G., Simulating reachability using first-order logic with applications to verification of linked data structures (2005) LNCS (LNAI), 3632, pp. 99-115. , Nieuwenhuis, R. (ed.) CADE 2005. Springer, Heidelberg
  • Lu, Y., Potter, J., A type system for reachability and acyclicity (2005) LNCS, 3586, pp. 479-503. , Gao, X.-X. (ed.) ECOOP 2005. Springer, Heidelberg
  • Neisen, A., (2010) Automatic Verification of Acyclic Data Structures Using Theorem Provers, , Master's thesis, Universidad de Buenos Aires
  • Sagiv, M., Reps, T., Wilhelm, R., Parametric shape analysis via 3-valued logic (2002) ACM TOPLAS, 24 (3), pp. 217-298
  • Smans, J., Jacobs, B., Piessens, F., VeriCool: An automatic verifier for a concurrent object-oriented language (2008) LNCS, 5051, pp. 220-239. , Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. Springer, HeidelbergA4 - DFG Deutsche Forschungsgemeinschaft; AbsInt Angewandte Informatik GmbH; Microsoft Research; Robert Bosch GmbH; IDS Scheer AG / Software AG

Citas:

---------- APA ----------
Garbervetsky, D., Gorín, D. & Neisen, A. (2011) . Enforcing structural invariants using dynamic frames. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, 6605 LNCS, 65-80.
http://dx.doi.org/10.1007/978-3-642-19835-9_8
---------- CHICAGO ----------
Garbervetsky, D., Gorín, D., Neisen, A. "Enforcing structural invariants using dynamic frames" . 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 6605 LNCS (2011) : 65-80.
http://dx.doi.org/10.1007/978-3-642-19835-9_8
---------- MLA ----------
Garbervetsky, D., Gorín, D., Neisen, A. "Enforcing structural invariants using dynamic frames" . 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, vol. 6605 LNCS, 2011, pp. 65-80.
http://dx.doi.org/10.1007/978-3-642-19835-9_8
---------- VANCOUVER ----------
Garbervetsky, D., Gorín, D., Neisen, A. Enforcing structural invariants using dynamic frames. Lect. Notes Comput. Sci. 2011;6605 LNCS:65-80.
http://dx.doi.org/10.1007/978-3-642-19835-9_8