Área: Engenharia Informática e de Computadores

Despacho de nomeação de Júri

Edital

Título da Tese: Automated Synthesis and Debugging of Declarative Programs

Local da Prova:  Anfiteatro PA-3 (Piso -1 do Pavilhão de Matemática) do IST 

Data: 20/07/2026

Hora: 14h30
Abstract: Declarative programming languages allow users to solve problems without explicitly defining control flow, yet this abstraction often makes writing and debugging code unintuitive for novices. This thesis explores automated reasoning techniques to support users in synthesizing and debugging programs across three declarative languages: Structured Query Language (SQL), Answer Set Programming (ASP), and Prolog. The first contribution is CUBES, a parallel synthesizer for SQL aimed at low-code platforms. Synthesizing queries from input-output examples is computationally intensive; CUBES addresses this by employing a divide-and-conquer enumeration strategy that exploits multi-core architectures. Furthermore, since examples often under-specify user intent, CUBES introduces an interactive disambiguation procedure. This process uses fuzzing to generate distinguishing inputs, allowing users to easily identify the correct query from multiple valid candidates, thereby significantly increasing synthesis accuracy. The second contribution, FormHe, targets the educational domain of Answer Set Programming. Debugging ASP is notoriously difficult due to its non-monotonic semantics. FormHe automates this process by computing Minimal Strongly Inconsistent Correction Subsets (MSICS) to localize faults. It then leverages constraint-based synthesis to repair faulty rules or generate missing ones. In evaluations using real student data, FormHe successfully identified and repaired faults in the majority of submissions, providing pedagogical hints that guide students toward correct solutions. Finally, the thesis presents ProDebug, an automated feedback tool for Prolog. Addressing the complexities of Prolog's unification and backtracking mechanisms, ProDebug combines traditional software engineering techniques - specifically Spectrum-based and Mutation-based Fault Localization - with fine-tuned Large Language Models. This hybrid architecture allows for precise bug detection and the generation of code repairs. Results confirm that ProDebug outperforms previous tools in Prolog fault localization accuracy and provides feedback that is valuable to students. Together, these systems demonstrate that combining formal logic methods with modern parallel computing and machine learning can significantly help users of different declarative programming languages in their tasks.