Plan

Nos juntamos con Diego y Dani. Charlamos de que venimos avanzando bastante bien y que podemos llegar a que me reciba en noviembre. Por supuesto que para eso hay que meterle porque faltan cerrar algunas cosas y además escribir todo.

De lo que falta hacer (en orden de prioridad) están las siguientes cosas:

• Implementar la idea de patrones de iteración que tienen un invariante conocido. De la mano de esto hay que buscar ejemplos donde estos patrones tienen sentido y evitan la escritura de un invariante potencialmente engorroso.

• Estrategias para elegir qué prover usar. Esto involucra probar varios demostradores distintos sobre cada fórmula, hasta que alguno pueda verificar la propiedad.

• Procedimientos.

• Syntax sugar para cuatificación más cómoda sobre elementos de arreglos, etc.

Además está la idea de escribir la tesis en inglés así ya se puede reutilizar una parte para armar algún artículo y presentarlo.

Esto hace que la idea de armar un plugin de eclipse quede postergada para después de que me reciba.