Tesis doctoral de Palasi Lallana Vicent Ramon
Se presenta un metodo de verificacion automatica llamado alice (algebraic inference of the correctness of environments). Dado un programa p y una especificacion algebraica sp1, alice determina si p es correcto respecto a sp1. Para hacer esto, alice construye primero una especificacion algebraica sp2 que es equivalente (es decir, tiene la misma semantica) a p. Asi, determinar la correccion de p respecto a sp1 se reduce a comprobar la equiValencia de dos especificaciones sp1 y sp2, segun una nueva nocion de equiValencia definida en la tesis. A partir de sp1 y sp2, alice construye una especificacion sp3 y un conjunto i de teoremas inductivos de forma que demostrar la equiValencia de sp1 y sp2 se reduce a demostrar i en el algebra inicial de sp3. De esta forma, alice determina la correccion de p respecto a sp1 comprobando (con un demostrador de teoremas inductivos) la satisfaccion de i en el algebra inicial de sp3. La principal novedad del metodo alice es que la verificacion es totalmente automatica y que, en lugar de trabajar comparando un programa y su especificacion, se hacen las transformaciones adecuadas para trabajar con dos especificaciones (que son objetos similares) y este hecho facilita notablemente el proceso alice no es un procedimiento de decision (ya que el problema es indecidible) y se puede extender para tratar otros problemas, como el de la equiValencia entre modulos.
Datos académicos de la tesis doctoral «Verificacio automatica de programes basada en semantica de comportament i logica de primer ordre: el metodo alice.«
- Título de la tesis: Verificacio automatica de programes basada en semantica de comportament i logica de primer ordre: el metodo alice.
- Autor: Palasi Lallana Vicent Ramon
- Universidad: Jaume i de castellón
- Fecha de lectura de la tesis: 01/01/1997
Dirección y tribunal
- Director de la tesis
- Francisco Toledo Lobo
- Tribunal
- Presidente del tribunal: Gregorio Martín Quetglas
- Vicent Botti Navarro (vocal)
- Buenaventura Clares (vocal)
- Del Pobil I Ferre Angel P. (vocal)