Thesis Title

Utilización del Slicing de Programas en la Validación y Modificación de Las Propiedades De Un Programa
Salvador V. Cavadini

Thesis Intro

La complejidad y tamaño del software implican una limitación para la verificación formal de sus propiedades, más aún cuando se trata de propiedades intrínsicamente difíciles de verificar como son, por ejemplo, las propiedades de seguridad y confidencialidad. La presente propuesta tiene por objetivo integrar la tecnología de slicing de programas al dominio de la verificación de programas. Creemos que el slicing puede ser utilizado para simplificar las pruebas de las propiedades de los programas a través de la división del mismo en subprogramas menos complejos y más fácilmente manejables en términos de la construcción de una demostración de sus propiedades. Para lograr esto es necesario, primero, estudiar en profundidad cómo utilizar las propiedades de los programas como criterios del proceso de slicing; también es preciso establecer qué propiedades del programa original son preservadas luego del proceso de slicing y estudiar la factibilidad de trasladar al programa original las verificaciones efectuadas sobre sus slices.
     

Thesis Info

Esta propuesta de trabajo está dirigida a determinar cómo combinar las técnicas de verificación –que son potentes y precisas pero requieren gran interacción con el usuario– y las técnicas de análisis estático de programas –que tienen un alto grado de automaticidad pero que son menos potentes y precisas– para obtener métodos de verificación precisos y suficientemente automáticos. Más específicamente, se propone estudiar cómo integrar el slicing de programas con técnicas de verificación como la demostración de teoremas y la interpretación abstracta para verificar las propiedades de programas codificados en lenguaje C. Esta investigación intentará responder las siguientes preguntas:

• ¿Qué tipo de propiedades pueden ser utilizadas como parámetros del proceso de slicing? ¿Cómo se utilizarán estas propiedades para extraer slices de programas?
• ¿Qué tipos de slices son los más útiles para la tarea de verificación de propiedades?
• ¿Qué propiedades del programa original son aún válidas luego del proceso de slicing?
• ¿Es posible transformar propiedades del programa original en propiedades de sus slices?

El slicing de programas, a menudo, es utilizado para la comprensión de programas aprovechando su capacidad para dividir el programa en partes funcionales menos complejas y manipulables de manera independiente. Es posible un aprovechamiento similar con el objeto de reducir la complejidad de las demostraciones de algunas propiedades. Es decir, ser capaces de obtener un slice de un programa P con respecto de una propiedad Q de tal manera que, si puede definirse una demostración de Q en el slice, entonces la propiedad Q es verdadera en P. Para lograr esto debe contestarse otra pregunta: ¿Las propiedades de un slice pueden trasladarse al programa original? Dar respuesta a estas preguntas significa un primer paso hacia la integración del slicing de programas a un entorno de verificación completo.

Thesis References

• Hiralal Agrawal. “On slicing programs with jump statements”. In Proceedings of the ACM SIGPLAN '94 Conference on Programming Language Design and Implementation, volume 29(6) of ACM SIGPLAN Notices, páginas 302-312, Orlando, FL, Junio 1994.
• Hiralal Agrawal, Richard A. DeMillo, y Eugene H. Spafford. “Dynamic slicing in the presence of unconstrained pointers”. Technical Report SERC-TR-93-P, Software Engineering Research Centre, Julio 1991.
• Alfred V. Aho, Ravi Sethi, Jefrey D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.
• Krzystof R Apt. “Ten Years of Hoare's Logic: A Survey—Part I”. ACM Transactions on Programming Languages and Systems, 3(4), pp. 431-483, October 1981.
• D. C. Atkinson y W. G. Griswold. “The design of whole-program analysis tools”. In Proceedings of the 18th International Conference on Software Engineering, pages 16-27, Berlin, Marzo 1996.
• Thomas Jaudon Ball. The Use of Control-Flow and Control-Dependence in Software Tools. PhD thesis, Computer Sciences Department, University of Wisconsin, Madison, 1993.
• Thomas Jaudon Ball y Susan B. Horwitz. “Slicing programs with arbitrary control flow”. In Proceedings of the First International Workshop on Automated and Algorithmic Debugging, volume 749 of Lecture Notes in Computer Science, pages 206-222, Heidelberg, Mayo 1993. Springer-Verlag.
• Nick Benton. “Simple relational correctness proofs for static analyses and program transformations”. ACM SIGPLAN Notices, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages POPL '04, Volume 39 Issue ,1 , 2004 .
• David Binkley. “Slicing in the presence of parameter aliasing”. In proceedings of the 1993 Software Engineering Research Forum, páginas 261-268, Orlando, FL, Noviembre 1993.
• David Binkley y Keith Brian Gallagher. “Program slicing”. In Advances in Computers, 1996.
• Andreas Blass; Gurevich Yuri. “The Underlying Logic of Hoare Logic”. Bulletin of the EATCS, Vol. 70, pp. 82-111, 2000.
• Rastislav Bodík y Rajiv Gupta. “Partial Dead Code Elimination using Slicing Transformations”. In Proceedings of the ACM SIGPLAN ‘97: Conference on Programing Languaje Design and Implementation (PLDI), Las Vegas, Nevada, Junio 1997.