Author name cluster

Pedro Resende

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

1 author row

FM Conference 2026 Conference Paper

Verifiably UX Compliant and User-Intent Layout Generation (Extended Abstract)

Joana Coutinho
Alexandre Lemos
Pedro Resende

Abstract Low-code platforms accelerate development of mission-critical applications, enabling users with less technical backgrounds to become proficient developers. AI-powered multi-agent systems further boost this experience. Large language models (LLMs) excel at understanding user intent, but alone cannot guarantee that design rules are followed - formal methods can provide such guarantees. We propose a hybrid approach that leverages both LLMs and a maximum satisfiability solver to generate layouts that comply with UX guidelines (e. g. , widget ordering and grouping rules) while respecting user intent. We evaluate the approach in production against an LLM-only baseline.

DOI

AAAI Conference 2024 Conference Paper

SAT-Based Algorithms for Regular Graph Pattern Matching

Miguel Terra-Neves
José Amaral
Alexandre Lemos
Rui Quintino
Pedro Resende
Antonio Alegria

Graph matching is a fundamental problem in pattern recognition, with many applications such as software analysis and computational biology. One well-known type of graph matching problem is graph isomorphism, which consists of deciding if two graphs are identical. Despite its usefulness, the properties that one may check using graph isomorphism are rather limited, since it only allows strict equality checks between two graphs. For example, it does not allow one to check complex structural properties such as if the target graph is an arbitrary length sequence followed by an arbitrary size loop. We propose a generalization of graph isomorphism that allows one to check such properties through a declarative specification. This specification is given in the form of a Regular Graph Pattern (ReGaP), a special type of graph, inspired by regular expressions, that may contain wildcard nodes that represent arbitrary structures such as variable-sized sequences or subgraphs. We propose a SAT-based algorithm for checking if a target graph matches a given ReGaP. We also propose a preprocessing technique for improving the performance of the algorithm and evaluate it through an extensive experimental evaluation on benchmarks from the CodeSearchNet dataset.

PDF Details DOI

I&C Journal 2012 Journal Article

An Algebra of Behavioural Types

António Ravara
Pedro Resende
Vasco T. Vasconcelos

We propose a process algebra, the Algebra of Behavioural Types, as a language for typing concurrent objects. A type is a higher-order labelled transition system that characterises all possible life cycles of a concurrent object. States represent interfaces of objects; state transitions model the dynamic change of object interfaces. Moreover, a type provides an internal view of the objects that inhabits it: a synchronous one, since transitions correspond to message reception. To capture this internal view of objects we define a notion of bisimulation, strong on labels and weak on silent actions. We study several algebraic laws that characterise this equivalence, and obtain completeness results for image-finite types.

Details DOI

TCS Journal 2003 Journal Article

Localic sup-lattices and tropological systems

Pedro Resende
Steven Vickers

The approach to process semantics using quantales and modules is topologized by considering tropological systems whose sets of states are replaced by locales and which satisfy a suitable stability axiom. A corresponding notion of localic sup-lattice (algebra for the lower powerlocale monad) is described, and it is shown that there are contravariant functors from sup-lattices to localic sup-lattices and, for each quantale Q, from left Q-modules to localic right Q-modules. A proof technique for third completeness due to Abramsky and Vickers is reset constructively, and an example of application to failures semantics is given.

Details DOI

TCS Journal 2001 Journal Article

Quantales, finite observations and strong bisimulation

Pedro Resende

It has often been claimed that bisimulation makes distinctions that cannot be observed in practice. Abramsky and Vickers proposed an algebraic framework based on quantales for describing observations on concurrent processes without hidden transitions and used it in order to provide an “observational explanation” of several process equivalences, ranging from Hoare trace equivalence to ready-simulation. We follow their approach and argue that (strong) bisimulation can be explained in the same way, at least in the case of “image-computable” labelled transition systems.

Details DOI