bachelorThesis
Técnicas basadas en búsqueda y aprendizaje para inferencia de especificaciones
Fecha
2022-02Autor
Molina, Facundo Joaquín
Institución
Resumen
La confiabilidad del software es una preocupación central en el proceso de construcción de software, y el análisis de la confiabilidad requiere una especificación del comportamiento esperado del software. Desafortunadamente, este análisis se ve afectado negativamente por la carencia de especificaciones acompañando el software. Con el objetivo de mejorar estos análisis de confiabilidad, en esta tesis presentamos técnicas basadas en búsqueda y aprendizaje para inferir especificaciones que permitan distinguir los comportamientos correctos de los comportamientos incorrectos del software, abordando el conocido problema del oráculo. Los enfoques que presentamos, basados principalmente en técnicas de aprendizaje como redes neuronales y computación evolutiva, son capaces de producir especificaciones que pueden capturar comportamientos complejos del software, y permiten lograr una mejora considerable en una serie de tareas de análisis de programas como bug finding, ejecución simbólica y verificación, entre otras. Software reliability is a primary concern in the software development process, and analyzing the software reliability requires the presence of specifications capturing the expected software behavior. Unfortunately, this analysis it's negatively affected by the lack of specifications accompanying the software. With the aim of improving software reliability analysis, in this dissertation we present search-based and learning-based techniques to infer specifications that allow to distinguish correct from incorrect software behaviors, tackling the well known oracle problem. The approaches that we present, based mainly in learning techniques such as neural networks and evolutionary computation, are capable of producing specifications that can capture complex software behaviors, and allow to achieve a considerable improvement on a number of program analysis tasks such as bug finding, symbolic execution and verification, among others.