Menu Content/Inhalt
Home arrow Seminarios arrow [5/6] Generación Automática de Invariantes Lineales
[5/6] Generación Automática de Invariantes Lineales

por Natalia Bidart

En el ámbito de las Ciencias de la Computación, se denomina *invariante* a la propiedad que se mantiene estable en un programa, en un determinado punto del mismo. Una *invariante de programa* es aquella que vale a lo largo de todo el programa. Consecuentemente, el descubrimiento de invariantes es una técnica central en el análisis y verificación de programas secuenciales y de sistemas reactivos.

Dado que el cálculo de invariantes posee una complejidad instrínseca, a lo largo del tiempo ha surgido la necesidad de automatizar ese proceso de cálculo.Variadas han sido las investigaciones y los resultados al respecto, destacando entre ellos los trabajos de R. Cousot [Cousto78], de N. Shankar [Shankar01], y de Z. Manna [Manna95].

El trabajo final a presentar tiene como objetivo implementar de manera genérica y eficiente el algoritmo propuesto por Cousot en [Cousto78].

Palabras clave:

  1. Poliedros convexos
  2. Programación
  3. Sistemas de Transiciones
  4. Postcondición más fuerte (SP)
  5. Sistemas Reactivos

Bibliografía:

[Cousot78] Patrick Cousot y Nicolas Halbwachs, “Automatic discovery of linear restraints among variables of a program”, 1978.

[Manna95] Nikolaj Bjorner y Anca Browne y Zohar Manna, “Automatic Generation of Invariants and Assertions”, 1995.

[Shankar01] A. Tiwari y H. Rues and H. Saidi y N. Shankar, “A Technique for Invariant Generation”, 2001.

 
< Anterior   Siguiente >
Content Management System: Joomla!
Template based on an original designed by www.madeyourweb.com