(T2) Language Agnostic Automated Program Verification in .Net using Static Analisys Tools (Verificación Automática de Programas en .Net usando Analizadores Estáticos)

cabezal
  • Profesor:  Francesco Logozzo (Microsoft Research, WA, USA)
  • Horario: Lunes a viernes de 13:30 a 16:30 horas
  • Aula: A definir (Pabellón 1)
  • Idioma: Inglés
  • Evaluación: Trabajo Práctico de tipo take-home

Resumen breve: Code Contracts es una manera de expresar pre y post-condiciones e invariantes de clase para la plataforma .NET. Este tipos de contratos sirven de documentación y para implementar aserciones de correctitud en tiempo de ejecución, pero también permiten la utilización de técnicas de verificación estática. Estas últimas convierten los contratos en especificaciones certificadas. Clousot es un verificador estático de Code Contracts basado en la técnica de interpretación abstracta. En este curso se introducirán y discutirán las decisiones de diseño y detalles formales de Code Contracts y Clousot.

Programa tentativo:  Día 1: Anotaciones en Code Contracts (contratos, invariantes, aserciones). Verificación en tiempo de ejecución. Día 2: Generación automática de anotaciones. Día 3: Introducción al análisis estático: interpretación abstracta. Día 4: Introducción al análisis estático: análisis del flujo de datos. Día 5: Verificación de contratos usando Clousot.

  • Bibliografía recomendada:

• Patrick Cousot & Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or
approximation of fixpoints. In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238—252, Los Angeles, California, 1977. ACM Press, New York.
• Vincent Laviron and Francesco Logozzo, SubPolyhedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities , in International Journal on Software Tools for Technology Transfer (STTT) , Springer Verlag, June 2011.
• Patrick Cousot, Radhia Cousot, and Francesco Logozzo, Contract Precondition Inference from Intermittent Assertions on Collections, in Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11), Springer Verlag, January 2011
• Manuel Fahndrich and Francesco Logozzo, Static contract checking with Abstract Interpretation, in Proceedings of the Conference on Formal Verification of Object-oriented Software (FoVeOOS 2010) , Springer Verlag, October 2010.
• Mike Barnett, Manuel Fahndrich, and Francesco Logozzo, Embedded Contract Languages, in ACM SAC - OOPS, Association for Computing Machinery, Inc., March 2010.
• Michael Barnett, Manuel Fahndrich, Francesco Logozzo, Peli de Halleux, and Nikolai Tillmann, Exploiting the Synergy between
Automated-Test-Generation and Programming-by-Contract, in Proc. 31st International Conference on Software Engineering (ICSE'2009), IEEE, May 2009.

Notas Finales

pie