El artículo presenta Diversify2Verify, una canalización por etapas basada en LLM para Why3 que genera implementaciones diversas de arreglos/listas recursivas e imperativas para mejorar la verificabilidad automatizada. El enfoque infiere contratos específicos de representación y emplea reparación de anotaciones guiada por verificador acotado para manejar fallos de verificación.
- Los autores construyeron un benchmark de 73 tareas sobre enteros, arreglos y listas, produciendo 292 variantes de implementación.
- Diversify2Verify verificó inicialmente 96 artefactos, aumentando a 154 después de dos pasadas de reparación.
- La verificación a nivel de artefacto mejoró del 32,9% al 52,7%.
- A nivel de tarea, al menos una variante se verificó para 49 de las 73 tareas, logrando una tasa de éxito del 67,1%.
Estos resultados demuestran que la diversidad de implementaciones ayuda a encontrar artefactos favorables a la verificación entre programas equivalentes por tarea.