reCipe: Un sintetizador de programas basado en Verificación de Modelos para Lógicas Temporales

Ponente(s): Fernando Abigail Galicia Mendoza, David A. Rosenblueth, Armando Solar-Lezama

El problema de Síntesis de Programas consiste en, dada una especificación de alto nivel (e.g. un fragmento de código o una especificación formal), un sistema devuelva de manera automática un programa que satisfaga dicha especificación. En esta plática presentaremos una alternativa de solución al problema de Síntesis de Programas utilizando técnicas de Verificación de Modelos para el caso de CTL (Lógica Computacional de Árbol). Dicha propuesta consiste en, dada una especificación en CTL (con cierta azúcar sintáctica) utilizar la semántica de los operadores EX y AX para que dado un FDS (Sistema Discreto con Equidad) con variables oráculo (variables que representan posibles expresiones del programa), utilizar el mecanismo del Verificador NuSMV para que este último calcule las expresiones que constituyen al programa. Estas expresiones son un contraejemplo de la especificación negada. Una vez finalizado este proceso, el sistema devolverá el programa que satisface la especificación original del usuario.