Sintetizando programas sin bucles con Rust y Z3
Synthesizing Loop-Free Programs with Rust and Z3 (2020)
La síntesis de programas busca automáticamente un programa que cumpla una especificación, pero el espacio de búsqueda es enorme. Este artículo explica la síntesis iterativa guiada por contraejemplos para programas sin bucles basados en componentes, siguiendo el trabajo de Gulwani et al. Incluye una implementación en Rust con el solver Z3 y analiza problemas de rendimiento en benchmarks difíciles.
Para algunos de los problemas de benchmark más difíciles, el sintetizador no logra encontrar una solución antes de que se me acabe la paciencia.