SMT-lib

Descubrí que el demostrador CVC viene con una característica que permite traducir a formato SMT-lib. Este es un formato que usan todos los demostradores SMT en una competencia que se hace una vez por año.

O sea, que ahora puedo escribir en SMT-lib gratis, sin esfuerzo porque el output a CVC ya lo tenía hecho.

Un tema es que varios demostradores, al leer archivos en este formato SMT-lib, sólo le dan bola a la primer propiedad que aparece ahí. Por eso ahora lo que hago es:

1. Ir acumulando las cosas que sé que son verdad (precondición y los asserts que surgen del flujo del programa).
2. Cuando encuentro un query lo parto en tantos átomos como elementos de la conjunción que denota.
3. Para cada átomo genero un archivo con todos los asserts acumulados como axiomas y pregunto si es teorema.
   
4. Si es teorema lo agrego al conjunto de axiomas. Sino, no.
5. Sigo hasta agotar todos los átomos de cada uno de los queries.

Al finalizar eventualmente hay algunas subfórmulas que no pudieron ser probadas.

Varios días pasaron

El jueves pasado di la charla sobre lo que estuve haciendo y en términos generales gustó. Hubo muchas preguntas (tal como esperábamos) sobre para qué sirve lo que estamos haciendo y cuál es la innovación, cuestiones que ni nosotros (Dani, Diego y yo) sabemos por ahora.

Estos días estuve yendo y viniendo con refactors al código hasta que me cansé y decidí que así como está es un código suficientemente malo y suficientemente bueno.

También estuve cursando una ECI con Shaz Qadeer, la verdad me está sirviendo muchísimo para aprender cosas nuevas y profundizar y entender otras que más o menos había visto en papers.

Le mostramos a Shaz lo que tenemos hecho y le pareció bien. Le pareció que la idea de Dani de hablar con demostradores de FOL es interesante, y vale la pena probar. Por eso estos días quiero ver de hacer algunos ejemplos, aunque sea a mano.

Para piter que lo mira por tevé

Se que piter cada tanto lee este blog. Piter, comprá la licuadora que debés.

Sin 'at'

A partir de lo que ví del artículo que mencionaba ayer, surgió un detalle que es no tratar más las variables dentro de estados tipo:

at(x,S0) ó at(y,S1)

Sino tratarlas con sufijos por ejemplo

x_S0 ó y_S1

De esta manera el demostrador se ahorra tener que trabajar con la función no interpreteada 'at' y posiblemente eso sea más rápido.

La contra: las aserciones descargadas al verificador son un poquito menos legibles.

Slides listas, PPL promete, un artículo

Por partes:

• Las slides para la charla de este jueves ya están cocinadas. Puede faltar pulir un poco, pero la base está.

• Estuve jugando con la interfaz para Java de la PPL. Probé BDDs y Poliedros (el otro día me di cuenta que en castellano van sin 'h'). Aparentemente la interfaz Java no tiene bindings para trabajar con Octágonos, incluso cuando éstos están implementados en la versión 0.10pre7 (que es la que obtuve del CVS). En estos días voy a ver si hago una interfaz propia para manejar de forma más o menos cómoda la interfaz de Java de la PPL. (Y también ver de que cuando le agreguen el soporte para Octágonos a la API de Java, poder incluirlo rápidamente en mi wrapper.)

• Estuve leyendo un artículo que promete ser interesante. Menciona una combinación entre SMT solvers e interpretación abstracta. La idea es discutir este artículo con Dani y Diego para ver qué se puede aprovechar de ahí.

PPL y preparando una charla

Estuve perdiendo bastante tiempo compilando una biblioteca o librería (como quieran llamarla) para manejar polihedros llamada PPL (Parma Polyhedra Library). Por suerte una vez concluido todo el asunto con éxito, pude engancharla con Java y ejecutar un pequeño test. Ahora debería empezar a montar una interfaz para trabajar contra esta o cualquier otra librería de polihedros.

Además estuve empezando a armar slides para dar una charla interna este jueves a la gente de la oficina. Dani y Diego me estuvieron dando una mano revisando lo que había hecho, que creo que está dentro de todo bien. Falta ampliar un poco algunas secciones y agregar algunas imágenes.

Frío, código y finde largo

¡Nieve en Buenos Aires! Tenía que decirlo, bueno, ahora lo "importante":

Durante el finde largo y las últimas horas de este martes que se va programé la verificación en tiempo de ejecución de los predicados tales como invariantes, precondiciones, etc. Falta verificar que los variantes decrecen.

De todas formas eso no es más que un pasatiempo para demorar las decisiones que tarde o temprano va a haber que tomar.

Por un lado quiero darle una segunda oportunidad a Simplify, un demostrador desarrollado por Compaq (cuando todavía existía) y que a Dani en un primer momento no le cerró, pero vi un par de personas que lo usan para cosas con cuantificadores (¡muchos cuantificadores!) y quiero ver cómo se comporta.

Por otro lado está la idea de usar mútiples demostradores en paralelo y ver cuál demuestra primero, de esta forma se aprovechan los puntos fuertes de cada uno.

Está también la idea, que debería empezar a delinear, de realizar ejecución simbólica de instrucciones sobre un dominio abstracto abstracto (sí, repetí abstracto).

Por último a mi me gustaría decidir cómo incorporar los arreglos. Una forma es dando un soporte genérico (instrucciones de store y load). Otra forma es dar una única operación sobre la cual podamos controlar un poco más, aunque no me queda muy claro cómo.

Ah, además Diego insiste (y con razón) en que lea un poco más, cosa que quiero hacer, pero una vez que haya decidido (más o menos) para donde encarar.

Cerrando la semana

Estuve laburando en integrar un demostrador genérico. Para no complicarse con librerias lo hago a travez de un llamado al programa y me engancho escribiendo en su input, leyendo su output desde java, lo cual permite integracion con cualquier demostrador para el cual contemos con:

• un ejecutable
• un convertidor de mis predicados a predicados en el lenguaje del demostrador
• un intérprete para la salida del demostrador que mapee a VALID, INVALID, UNKNOWN

También estuve generando código java a partir de nuestros programas y lo que quedó funciona muy bien (¡incluso los genera sin warnings!). Lo que por ahora (por falta de tiempo) no hace es generar código (assertions) que verifiquen que las pre y post valen en tiempo de ejecución.

Por último estuve jugando con los dos demostradores (yices y cvc) para ver que tanto se bancan arrays y cuatificadores. En mi experiencia cada vez que digo algo cuantificado universalmente la respuesta es unknown. Realmente estoy empezando a dudar seriamente de que algo con arrays pueda llegar siquiera a hacerse (siempre y cuando nos quedemos en el mundo de los demostradores automáticos). En caso de que esto sea tan malo como parece, creo que vamos a necesitar un "plan b"... porque introducir arrays sería equivalente a demostrar todos los programas EXCEPTO aquellos que tienen arrays... algo bastante ridículo.

Un nuevo demostrador, velitas y desilución

El martes leyendo por ahí alguna web que ya no recuerdo, encontré un demostrador que se llama Yices, que le gana a todo el resto según los resultados de una competencia llamada SMT-COMP.

El miércoles cumplí 24 años. A pesar de que estuve en la facu un rato, mucho no laburé.

El jueves, o sea, hoy, implementé el binding necesario para utilizar este otro demostrador. Y me llevé una triste sorpresa al comprobar que no soporta bajo ningún concepto aritmética no lineal. O sea... que no me sirve para casi nada...

Sin procedimientos

Después de charlar con Diego y Dani llegamos a la conclusión de que por lo pronto iremos para adelante sin procedimientos, volviendo a la vieja idea de los bloques con pre y postcondiciones.

Hoy programé un rato y finalmente lo tengo andando: verifica loops y todo.

Además me contestó la gente de CVC3, diciendo que todavía no tuvieron tiempo de ver un bug report que les envié, pero que cualquier novedad me lo harían saber.

¿Procedimientos?

Después de varios días de reestructurar código llegué a una especie de callejón sin salida al querer implementar bloques con pre y post condiciones.

No queda claro qué cosas modifican y qué cosas no y cómo vincular esto con el resto del código que envuelve ese bloque.

Una forma posible de resolverlo es definir muy claramente cuál es la semántica con la que queremos trabajar con dichos bloques, pero creo que el problema es equivalente al de definir una semántica formal para trabajar con procedimientos.

Por lo tanto se me ocurre que es mejor optar por empezar a manejar procedimientos y matar dos pájaros de un tiro.