Formal Methods

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