Registro:
| Documento: | Tesis de Grado |
| Título: | Verificación automática de estructuras de datos acíclicas usando demostradores de teoremas |
| Título alternativo: | Automatic verification of acyclic data structures using theorem provers |
| Autor: | Neisen, Ariel Martín |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la web: | 2025-06-12 |
| Fecha de defensa: | 2010 |
| Fecha en portada: | 2010 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Garbervetsky, Diego David |
| Director Asistente: | Gorin, Daniel Alejandro |
| Jurado: | Bonelli, Eduardo Augusto; Caso, Guido de |
| Idioma: | Español |
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/seminario_nCOM000751_Neisen |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000751_Neisen.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000751_Neisen |
| Ubicación: | Dep.COM 000751 |
| Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Neisen, Ariel Martín. (2010). Verificación automática de estructuras de datos acíclicas usando demostradores de teoremas. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/seminario_nCOM000751_Neisen |
Resumen:
El objetivo de la presente tesis es investigar acerca del diseño de lenguajes orientados a objetos y las diferentes técnicas existentes para ofrecer garantías estáticas de verificación. En particular, nos interesa definir un calificador de tipos acíclicos, que asegure que la clausura transitiva de la relación points-to de una instancia acíclica sea irreflexiva. Listas enlazadas y árboles son típicos ejemplos de tipos acíclicos. Dicha propiedad es interesante debido a que: i) las estructuras de datos acíclicas pueden ser fácilmente recolectadas utilizando una estrategia de conteo de referencias (reference counting), y ii) es sencillo garantizar la terminación de ciclos que recorren estructuras de datos acíclicas. La discusión sobre la aciclicidad nos llevará a entender cuán difícil es garantizar con las herramientas disponibles en la actualidad. Desde el punto de vista técnico, propusimos un lenguaje con un calificador de clases opcional "acíclico". El mismo impone algunas restricciones de tipado: si la clase A es declarada como acíclica y A contiene un campo "f" de tipo B, entonces B debe ser acíclico también. La aciclicidad es entonces forzada por construcción, o sea, agregando una precondición especial a la asignación "a.f: = b", para "a" una instancia acíclica, que garantice la preservación de la aciclicidad de "a" y "b". La especificación es lograda utilizando una variación del trabajo realizado en dynamic frames. Uno de los problemas más interesantes a resolver es encontrar el nivel correcto de abstracción, en particular, cuál es la mínima información necesaria en el contrato de los métodos para que funcione correctamente la verificación. El trabajo sobre Dynamic Frames ofrece un enfoque elegante para resolverlo. Las contribuciones de esta tesis incluyen la presentación de un nuevo lenguaje, con la definición formal de su semántica y las pruebas de su validez. Finalmente, se analizan experiencias realizadas que aprovechan los beneficios de los tipos acíclicos.
Abstract:
The aim of this thesis is to research on the design of object-oriented languages and the different techniques available to offer static verification guarantees. In particular, we became interested in defining acyclic type qualifier. By this we mean that the transitive closure of the points-to relation of an instance of an acyclic type must be irreflexive. Linked-lists and trees constitute typical examples of acyclic types. This is interesting because: i) acyclic data structures can be garbage collected automatically using a cheap reference counting strategy, and ii) loops that traverse acyclic data structures can be easily shown to be terminating. The discussion on acyclicity will lead us to understand how difficult it is to verify it using the current techniques available. Technically speaking, we propose a language with an optional "acyclic" qualification to the classes declaration. This imposes some typing constraints: if class A is declared as acyclic and A contains a field "f" of type B, then B must have been declared as acyclic too. Acyclicity is then enforced by construction, that is, by adding a special precondition to the assignment "a.f: = b" for "a" an instance of an acyclic type, that guarantees that the a.cyclicity of "a" and "b" are preserved. The specification is achieved by using a variation of the dynamic frames style. One interesting problem is to find the right level of abstraction: wha.t is the minimum information needed to include in the contract of each method to make the verification work. The link with the specification of Dynamic Frames offers an elegant approach to help here. The contributions of the work include the presentation of the new language, with the formal definition of its semantics and the proofs of soundness. We end up analyzing the experimental code samples, taking advantage of the acyclic types benefits.
Citación:
---------- APA ----------
Neisen, Ariel Martín. (2010). Verificación automática de estructuras de datos acíclicas usando demostradores de teoremas. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000751_Neisen
---------- CHICAGO ----------
Neisen, Ariel Martín. "Verificación automática de estructuras de datos acíclicas usando demostradores de teoremas". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2010.https://hdl.handle.net/20.500.12110/seminario_nCOM000751_Neisen
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000751_Neisen.pdf
Distrubución geográfica
