Formal Methods

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 @ SAT 2023 featured image

UpMax: User partitioning for MaxSAT @ SAT 2023

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 @ VLDB 2020 featured image

SQUARES: A SQL Synthesizer Using Query Reverse Engineering @ VLDB 2020

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 @ CP 2019 featured image

Encodings for Enumeration-Based Program Synthesis @ CP 2019

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
Encodings for Enumeration-Based Program Synthesis featured image

Encodings for Enumeration-Based Program Synthesis

In this paper, a new compact line-based encoding is proposed that allows a faster enumeration of the program space.

avatar
Pedro Orvalho
Read more