Uso de especificaciones para superar las limitaciones de la reparación automatizada de programas basada en pruebas

Automated program repair often relies on syntactic transformations, generating large numbers of fix candidates whose correctness must be validated. Due to the combinatorial explosion of candidate combinations, existing techniques typically avoid exhaustive exploration and restrict intra-statement modifications, limiting their effectiveness. Moreover, patch validation commonly relies on test suites, which can lead to the acceptance of incorrect fixes due to overfitting. This problem persists even in modern approaches based on large language models (LLMs), which also face challenges of correctness and generalization. In this thesis, we first investigate the reliability of test suites as acceptance criteria. Using a bug-finding tool, we analyze patches produced by GenProg, Angelix, AutoFix, and Nopol on the IntroClass benchmark, across varying test suite qualities. Our study reveals that a majority of accepted patches are incorrect when validated against formal specifications, demonstrating that spurious fixes are frequently accepted, that overfitting remains significant even with larger test suites, and that semantics-based tools underestimate overfitting. To address these limitations, we introduce Stryker, a repair technique for contract-equipped programs. Stryker exhaustively explores intra-statement syntactic mutations up to a bounded depth, combining runtime analysis with bounded verification. It incorporates a novel contract-based pruning mechanism to discard infeasible candidates early, mitigating the explosion of the search space. Experiments show that Stryker repairs 56% of programs on the IntroClass benchmark (median variant) while eliminating up to 99% of the candidate space through contract-based pruning, avoiding thousands of invalid fixes that would pass test-based validation. To improve scalability, we develop Distributed Stryker, which parallelizes the candidate pruning process across multiple machines. Evaluation demonstrates speedups of up to 54x with 32 machines on programs with multiple faults, while preserving the correctness guarantees of the sequential approach. In conclusion, this thesis highlights both the limitations of current APR methodologies and the potential of bounded, contract-guided search to improve the reliability and generality of these techniques. By combining exhaustive syntactic exploration with formal specifications and distributed verification, this work lays the foundation for a new generation of automated repair systems that are more precise and offer stronger correctness guarantees within bounded analysis scopes. The relevance of this work is further reinforced by recent advances in automated specification generation via large language models, which present promising directions for overcoming the limitation of formal contract availability and enabling broader applicability of contract-based repair. Muchas técnicas de reparación automática de programas aplican transformaciones sintácticas para generar grandes cantidades de candidatos de reparación, cuya corrección debe ser verificada. Debido a la explosión combinatoria de candidatos, las técnicas existentes típicamente evitan una exploración exhaustiva y restringen las modificaciones intra-sentencia, limitando así su efectividad. Además, la validación de parches generalmente se basa en conjuntos de pruebas, lo cual puede conducir a la aceptación de reparaciones incorrectas debido a sobreajuste. Este problema persiste incluso en enfoques modernos basados en modelos de lenguaje de gran escala (LLMs), que también enfrentan desafíos de corrección y generalización. En esta tesis, primero investigamos la confiabilidad de los conjuntos de pruebas como criterio de aceptación. Utilizando una herramienta de detección de errores, analizamos parches producidos por GenProg, Angelix, AutoFix y Nopol en el benchmark IntroClass, considerando distintas calidades de conjuntos de pruebas. Nuestro estudio revela que la mayoría de los parches aceptados son incorrectos cuando se validan con especificaciones formales, demostrando que las reparaciones espurias son frecuentemente aceptadas, que el sobreajuste sigue siendo significativo incluso con conjuntos de pruebas más grandes, y que las herramientas basadas en semántica subestiman la magnitud del sobreajuste. Para abordar estas limitaciones, introducimos Stryker, una técnica de reparación para programas equipados con contratos. Stryker explora exhaustivamente mutaciones sintácticas intra-sentencia hasta una profundidad acotada, combinando análisis en tiempo de ejecución con verificación acotada. Incorpora un novedoso mecanismo de poda basado en contratos para descartar tempranamente candidatos inviables, mitigando así la explosión del espacio de búsqueda. Los experimentos muestran que Stryker repara el 56% de los programas del benchmark IntroClass (variante median) mientras evita miles de reparaciones inválidas que pasarían una validación basada en pruebas, eliminando hasta el 99% del espacio de candidatos mediante poda basada en contratos. Finalmente, para mejorar la escalabilidad, desarrollamos Distributed Stryker, que paraleliza el proceso de poda de candidatos en múltiples máquinas. La evaluación demuestra aceleraciones de hasta 54x con 32 máquinas en programas con múltiples fallas, manteniendo las garantías de corrección del enfoque secuencial. En conclusión, esta tesis resalta tanto las limitaciones de las metodologías actuales de reparación automática de programas como el potencial de las búsquedas acotadas y guiadas por contratos para mejorar la confiabilidad y generalidad de estas técnicas. Combinando una exploración sintáctica exhaustiva con especificaciones formales y verificación distribuida, este trabajo sienta las bases para una nueva generación de sistemas de reparación automática: más precisos y con garantías de corrección más fuertes dentro del alcance del análisis acotado. La relevancia de este trabajo se ve reforzada por los recientes avances en generación automática de especificaciones mediante LLMs, que abren oportunidades para superar la limitación de disponibilidad de contratos formales y permitir una mayor aplicabilidad de la reparación basada en contratos.