Formal Methods

MENTOR: Automated Feedback for Introductory Programming Exercises featured image

MENTOR: Automated Feedback for Introductory Programming Exercises

This PhD thesis presents MENTOR, a semantic automated program repair (APR) framework designed to provide Automated Feedback for Introductory Programming Exercises.

avatar
Pedro Orvalho
Read more
Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization featured image

Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization

In this paper, we propose a novel approach that combines the strengths of both FM-based fault localization and LLMs, via zero-shot learning, to enhance APR for IPAs. Our method …

avatar
Pedro Orvalho
Read more
Model-Based Diagnosis for Software featured image

Model-Based Diagnosis for Software

Localising system faults has long been recognised as one of the most time-consuming and costly tasks in software engineering. Given a buggy system, fault localisation (FL) refers …

avatar
Pedro Orvalho
Read more
📄 Paper accepted @ AAAI 2025!! 🎉 featured image

📄 Paper accepted @ AAAI 2025!! 🎉

I am very happy to share that our paper that combines the strengths of both MaxSAT-based fault localisation and Large Language Models, via zero-shot learning, to enhance automated …

avatar
Pedro Orvalho
Read more
Automated Feedback for Introductory Programming Exercises featured image

Automated Feedback for Introductory Programming Exercises

Delivering valuable and personalised feedback to students remains one of the greatest challenges in programming education, particularly in courses with large enrollments. Providing …

avatar
Pedro Orvalho
Read more
CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases featured image

CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases

In this talk I will introduce a novel fault localization approach for C programs with multiple faults. CFaults leverages Model-Based Diagnosis (MBD) with multiple observations and …

avatar
Pedro Orvalho
Read more
CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases featured image

CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases

This paper introduces a novel fault localization approach for C programs with multiple faults. CFaults leverages Model-Based Diagnosis (MBD) with multiple observations and …

avatar
Pedro Orvalho
Read more
User partitioning for Maximum Satisfiability featured image

User partitioning for Maximum Satisfiability

The Maximum Satisfiability (MaxSAT) problem is the optimisation variant of the Satisfiability (SAT) problem. Solving MaxSAT efficiently often involves partitioning the set of soft …

avatar
Pedro Orvalho
Read more
UpMax: User partitioning for MaxSAT featured image

UpMax: User partitioning for MaxSAT

In this talk I will present a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms.

avatar
Pedro Orvalho
Read more
UpMax: User partitioning for MaxSAT featured image

UpMax: User partitioning for MaxSAT

This paper proposes a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms. As a result, new partitioning procedures can be …

avatar
Pedro Orvalho
Read more

AlloyMax: Bringing Maximum Satisfaction to Relational Specifications

We propose AlloyMax, an extension of Alloy with a capability to express and analyze problems with optimal solutions. AlloyMax introduces (1) a small addition of language constructs …

Changjian Zhang
Read more
SQUARES: A SQL Synthesizer Using Query Reverse Engineering featured image

SQUARES: A SQL Synthesizer Using Query Reverse Engineering

In this talk I present SQUARES, an open-source tool that generates SQL and R queries from specifications. The specifications are expressed with input-output tables and some …

avatar
Pedro Orvalho
Read more
SQUARES: A SQL Synthesizer Using Query Reverse Engineering featured image

SQUARES: A SQL Synthesizer Using Query Reverse Engineering

In this paper, we present SQUARES, an open-source tool that generates SQL and R queries from specifications. The specifications are expressed with input-output tables and some …

avatar
Pedro Orvalho
Read more
SQUARES: A SQL Synthesizer Using Query Reverse Engineering featured image

SQUARES: A SQL Synthesizer Using Query Reverse Engineering

MSc Thesis. We propose a novel Enumeration-Based SQL synthesizer SQUARES, that uses a new line representation where we represent each program line with its own subtree.

avatar
Pedro Orvalho
Read more
Encodings for Enumeration-Based Program Synthesis featured image

Encodings for Enumeration-Based Program Synthesis

In this talk I will present a new compact line-based encoding is proposed that allows a faster enumeration of the program space.

avatar
Pedro Orvalho
Read more